Dr Andrei Popescu

PhD

Department of Computer Science

Senior Lecturer in Cybersecurity

Course Director for MSc Cybersecurity and AI

Member of the Security of Advanced Systems research group

Affiliate member of the Security of Advanced Systems research group

a.popescu@sheffield.ac.uk
+44 114 222 1967

Regent Court (DCS)

Full contact details

Dr Andrei Popescu
Department of Computer Science
Regent Court (DCS)
211 Portobello
Sheffield
S1 4DP

Profile: Andrei has been a Senior Lecturer in the Security of Advanced Systems group since May 2020. Previously, he worked as a Senior Lecturer at Middlesex University and as a postdoctoral researcher at TU Munich. He has a Ph.D. in computer science from the University of Illinois at Urbana-Champaign and a Ph.D. in mathematics from the University of Bucharest.

Research interests

Proof assistants
Information flow security
Inductive and coinductive datatypes
Automated deduction
Syntax with bindings

Publications

Journal articles

Popescu A & Traytel D (2023) Admissible Types-to-PERs Relativization in Higher-Order Logic. Proceedings of the ACM on Programming Languages, 7(POPL), 1214-1245.
Popescu A & Traytel D (2021) Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant. Journal of Automated Reasoning, 65(7), 1027-1070. View this article in WRRO
Popescu A, Peter L & Ping H (2020) CoCon: A conference management system with verified document confidentiality. Journal of Automated Reasoning. View this article in WRRO
Gheri L & Popescu A (2020) A formalized general theory of syntax with bindings: extended version. Journal of Automated Reasoning, 64(4), 641-675.
Blanchette JC, Gheri L, Popescu A & Traytel D (2019) Bindings as bounded natural functors. Proceedings of the ACM on Programming Languages, 3(POPL). View this article in WRRO
Kunčar O & Popescu A (2019) From types to sets by local type definition in higher-order logic. Journal of Automated Reasoning, 62(2), 237-260.
Kunčar O & Popescu A (2019) A consistent foundation for Isabelle/HOL. Journal of Automated Reasoning, 62(4), 531-555.
Avigad J, Blanchette JC, Klein G, Paulson L, Popescu A & Snelting G (2018) Introduction to Milestones in Interactive Theorem Proving. Journal of Automated Reasoning, 61(1-4), 1-8.
Kunčar O & Popescu A (2018) Safety and conservativity of definitions in HOL and Isabelle/HOL. Proceedings of the ACM on Programming Languages, 2(POPL). View this article in WRRO
Bauereiß T, Pesenti Gritti A, Popescu A & Raimondi F (2018) CoSMed: a confidentiality-verified social media platform. Journal of Automated Reasoning, 61(1-4), 113-139.
Blanchette J, Böhme S, Popescu A & Smallbone N (2017) Encoding monomorphic and polymorphic types. Logical Methods in Computer Science, 12(4), 1-52. View this article in WRRO
Blanchette JC, Popescu A & Traytel D (2017) Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58(1), 149-179.
Blanchette JC, Popescu A & Traytel D (2015) Foundational extensible corecursion: a proof assistant perspective. ACM SIGPLAN Notices, 50(9), 192-204.
Popescu A & Roşu G (2015) Term-generic logic. Theoretical Computer Science, 577, 1-24.
Blanchette JC, Popescu A & Traytel D (2015) Witnessing (Co)datatypes, 359-382.
Nipkow T & Popescu A (2014) Making security type systems less ad hoc. it - Information Technology, 56(6), 267-272.
Popescu A, Hölzl J & Nipkow T (2013) Formal verification of language-based concurrent noninterference. Journal of Formalized Reasoning, 6(1), 1-30.
Popescu A & Gunter EL (2011) Recursion principles for syntax with bindings and substitution. ACM SIGPLAN Notices, 46(9), 346-358.
Popescu A, Şerbănuţă TF & Roşu G (2009) A semantic approach to interpolation. Theoretical Computer Science, 410(12-13), 1109-1128.
Popescu A (2007) Some algebraic theory for many-valued relation algebras. Algebra universalis, 56(2), 211-235.
Gâinâ D & Popescu A (2007) An Institution-Independent Proof of the Robinson Consistency Theorem. Studia Logica, 85(1), 41-73.
Georgescu G & Popescu A (2006) A new class of probabilities on Łukasiewicz-Moisil algebras. Journal of Multiple-Valued Logic and Soft Computing, 12(3-4 SPEC. ISS.), 337-354.
Georgescu G & Popescu A (2006) A common generalization for MV-algebras and Łukasiewicz–Moisil algebras. Archive for Mathematical Logic, 45(8), 947-981.
Georgescu G, Leuştean I & Popescu A (2006) Order convergence and distance on Łukasiewicz-Moisil algebras. Journal of Multiple-Valued Logic and Soft Computing, 12(1-2), 33-69.
Popescu A (2005) Łukasiewicz-Moisil Relation Algebras. Studia Logica, 81(2), 167-189.
Popescu A (2005) Many-valued relation algebras. Algebra universalis, 53(1), 73-108.
Georgescu G & Popescu A (2004) Non-dual fuzzy connections. Archive for Mathematical Logic, 43(8), 1009-1039.
Georgescu G & Popescu A (2004) Non-commutative fuzzy structures and pairs of weak negations. Fuzzy Sets and Systems, 143(1), 129-155.
Popescu A (2004) A general approach to fuzzy concepts. MLQ, 50(3), 265-280.
Georgescu G & Popescu A (2003) Non-commutative fuzzy Galois connections. Soft Computing, 7(7), 458-467.
Georgescu G & Popescu A (2002) Concept lattices and similarity in non-commutative fuzzy logic. Fundamenta Informaticae, 53(1), 23-54.
Popescu A () Supernominal Datatypes and Codatatypes. Electronic Proceedings in Theoretical Computer Science, 332.
() An Institution-independent Generalization of Tarski's Elementary Chain Theorem. Journal of Logic and Computation, 17(3), 605-605.
Gaina D & Popescu A () An Institution-independent Generalization of Tarski's Elementary Chain Theorem. Journal of Logic and Computation, 16(6), 713-735.

Chapters

Popescu A & Roşu G (2009) Term-Generic Logic, Recent Trends in Algebraic Development Techniques (pp. 290-307). Springer Berlin Heidelberg
Popescu A, Şerbănuţă TF & Roşu G (2006) A Semantic Approach to Interpolation, Lecture Notes in Computer Science (pp. 307-321). Springer Berlin Heidelberg
Popescu A & Roşu G (2005) Behavioral Extensions of Institutions, Algebra and Coalgebra in Computer Science (pp. 331-347). Springer Berlin Heidelberg

Conference proceedings papers

Popescu A (2022) Rensets and renaming-based recursion for syntax with bindings. Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings (pp 618-639). Haifa, Israel, 8 August 2022 - 10 August 2022.
Popescu A, Bauereiss T & Lammich P (2021) Bounded-deducibility security. 12th International Conference on Interactive Theorem Proving (ITP 2021), Vol. 193 (pp 3:1-3:20). Online, 29 June 2021 - 1 July 2021. View this article in WRRO
Popescu A & Traytel D (2019) A formally verified abstract account of Gödel’s incompleteness theorems. Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings (pp 442-461). Natal, Brazil, 27 August 2019 - 30 August 2019.
Biendarra J, Blanchette JC, Bouzy A, Desharnais M, Fleury M, Hölzl J, Kunčar O, Lochbihler A, Meier F, Panny L , Popescu A et al (2017) Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic (pp 3-21)
Gheri L & Popescu A (2017) A formalized general theory of syntax with bindings. Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, Vol. 10499 (pp 241-261). Brasília, Brazil, 26 September 2017 - 29 September 2017.
Blanchette JC, Meier F, Popescu A & Traytel D (2017) Foundational nonuniform (Co)datatypes for higher-order logic. 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland, 20 June 2017 - 23 June 2017.
Bauereiß T, Gritti AP, Popescu A & Raimondi F (2017) CoSMeDis : a distributed social media platform with formally verified confidentiality guarantees. 2017 IEEE Symposium on Security and Privacy (SP) (pp 729-748). San Jose, CA, USA, 22 May 2017 - 26 May 2017. View this article in WRRO
Blanchette JC, Bouzy A, Lochbihler A, Popescu A & Traytel D (2017) Friends with benefits: implementing corecursion in foundational proof assistants. Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Vol. LNTCS,volume 10201 (pp 111-140). Uppsala, Sweden, 22 April 2017 - 29 April 2017.
Kunčar O & Popescu A (2017) Comprehending Isabelle/HOL’s Consistency. Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Vol. LNTCS,volume 10201 (pp 724-749). Uppsala, Sweden, 22 April 2017 - 29 April 2017.
Bauereiß T, Pesenti Gritti A, Popescu A & Raimondi F (2016) CoSMed: a confidentiality-verified social media platform. Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, Vol. LNTCS,volume 9807 (pp 87-106). Nancy, France, 22 August 2016 - 25 August 2016.
Kunčar O & Popescu A (2016) From types to sets by local type definitions in higher-order logic. Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, Vol. LNTCS,volume 9807 (pp 200-218). Nancy, France, 22 August 2016 - 25 August 2016.
Kunčar O & Popescu A (2015) A Consistent Foundation for Isabelle/HOL (pp 234-252)
Blanchette JC, Popescu A & Traytel D (2015) Foundational extensible corecursion: a proof assistant perspective. Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming - ICFP 2015, 31 August 2015 - 2 September 2015. View this article in WRRO
Blanchette JC, Popescu A & Traytel D (2014) Unified Classical Logic Completeness (pp 46-60)
Kanav S, Lammich P & Popescu A (2014) A Conference Management System with Verified Document Confidentiality (pp 167-183)
Blanchette JC, Popescu A & Traytel D (2014) Cardinals in Isabelle/HOL (pp 111-127)
Blanchette JC, Hölzl J, Lochbihler A, Panny L, Popescu A & Traytel D (2014) Truly Modular (Co)datatypes for Isabelle/HOL (pp 93-110)
Schropp A & Popescu A (2013) Nonfree Datatypes in Isabelle/HOL (pp 114-130)
Popescu A, Hölzl J & Nipkow T (2013) Formalizing Probabilistic Noninterference (pp 259-275)
Blanchette JC & Popescu A (2013) Mechanizing the Metatheory of Sledgehammer (pp 245-260)
Blanchette JC, Böhme S, Popescu A & Smallbone N (2013) Encoding Monomorphic and Polymorphic Types (pp 493-507)
Popescu A, Hölzl J & Nipkow T (2013) Noninterfering Schedulers (pp 236-252)
Popescu A, Hölzl J & Nipkow T (2012) Proving Concurrent Noninterference (pp 109-125)
Traytel D, Popescu A & Blanchette JC (2012) Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. 2012 27th Annual IEEE Symposium on Logic in Computer Science, 25 June 2012 - 28 June 2012.
Blanchette JC, Popescu A, Wand D & Weidenbach C (2012) More SPASS with Isabelle (pp 345-360)
Popescu A & Gunter EL (2011) Recursion principles for syntax with bindings and substitution. Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
Popescu A & Gunter EL (2010) Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization (pp 109-127)
Popescu A, Gunter EL & Osborn CJ (2010) Strong Normalization for System F by HOAS on Top of FOAS. 2010 25th Annual IEEE Symposium on Logic in Computer Science, 11 July 2010 - 14 July 2010.
Gunter EL, Osborn CJ & Popescu A (2009) Theory support for weak higher order abstract syntax in Isabelle/HOL. Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice - LFMTP '09, 2 August 2009 - 2 August 2009.
Popescu A (2009) Weak Bisimilarity Coalgebraically (pp 157-172)
Georgescu G & Popescu A (2005) Similarity Convergence in Residuated Structures. Logic Journal of the IGPL, Vol. 13(4) (pp 389-413)

Preprints

Gheri L & Popescu A (2021) Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS, arXiv.
Gheri L & Popescu A (2017) A Formalized General Theory of Syntax with Bindings, arXiv.
Blanchette JC, Böhme S, Popescu A & Smallbone N (2016) Encoding Monomorphic and Polymorphic Types, arXiv.
Blanchette JC, Popescu A & Traytel D (2015) Foundational Extensible Corecursion, arXiv.

Grants

Current Grants

Security of Digital Twins in Manufacturing, EPSRC, 10/2021 - 04/2024, £774,954, as Co-PI
Cyclic Reasoning Mechanisms for Interactive Theorem Proving, Royal Society, 08/2021 - 07/2023, £12,000, as PI

Previous Grants

2019–2020 Principal investigator for VeTSS grant “Formal Verification of Information Flow Security for Relational Databases” (£86 198)
2016–2018 Principal investigator for EPSRC grant “Verification of Web-based Systems (VOWS),” acquired via the first grant scheme (£100 933)