I am a senior lecturer (associate professor) in the Security of Advanced Systems research group of the Department of Computer Science at the University of Sheffield. Previously, I worked as a lecturer at Middlesex University and as a postdoctoral researcher at TU Munich, in the Chair for Logic and Verification headed by Tobias Nipkow and patroned by goddess Isabelle. Further down in the past, I did my Ph.D. in computer science at the University of Illinois at Urbana-Champaign, advised by Elsa L. Gunter and Grigore Roșu. Even further back, when I was really really young, I did my Ph.D. in mathematics at the University of Bucharest, advised by George Georgescu.


Contents:  News and events ⋅ Recorded talks and lectures ⋅ Teaching ⋅ Resources for students ⋅ Research ⋅ Publications ⋅ Theses ⋅ Edited volumes ⋅ Formal proofs ⋅





News and events I am involved in

Please click here for some older news





Some recorded talks and lectures



Current courses taught at University of Sheffield



Courses taught in the past (at Middlesex University)
  • Testing and Verification (third year course, 2019-2020)
  • Decision Support Systems (second year course, 2016-2020)
  • Web Development (second year course, 2014-2016)
  • Software Development (second year course, 2014–2016)




Resources for students

Some miscellaneous material can be found on this page. For material on the currently taught courses please see the university page.

My lectures and Isabelle exercise sheets from the Midlands Graduate School (MGS) 2021 can be found here.




Research

My research topics are proof assistants, inductive and coinductive datatypes, automated deduction, syntax with bindings and information flow security.

● In Munich, I was the initiator of a project aimed at designing and implementing a modular datatype specification mechanism for Isabelle/HOL, covering state-of-the-art mutual and nested inductive and coinductive datatypes based on insight from category theory. The project's success, measured in the large and growing number of happy users of the new (co)datatype package, is largely due to my brilliant collaborators, Jasmin Blanchette and Dmitriy Traytel, who contributed to the design and did most of the implementation. Other colleagues have also contributed. Our results, summarized (and some anticipated) in my ESOP'15 slides, have been reported in several papers: LICS'12, IJCAR'14, ITP'14, ESOP'15, ICFP'15, ESOP'17, LICS'17. Some of my related work includes non-free datatypes (CPP'13) and syntax with bindings (LICS'10, ICFP'11, TCS 2015). In recent work (POPL'19), which forms the topic of Lorenzo Gheri's PhD thesis, we have been merging the syntax with bindings theme and the modular (co)inductive datatypes theme.

● I also work on the logical foundations of proof assistants based on higher-order logic. In particular, Isabelle/HOL extends the traditional version of HOL used in theorem proving (due to Mike Gordon) in a non-trivial way to accommodate ad hoc overloading. In turn, this enables Haskel-style type classes, leading to lighter developments. One could even argue that type classes are a key ingredient behind Isabelle/HOL's popularity. Together with Ondřej Kunčar, I have shown that Isabelle/HOL's logic is consistent, by two alternative proofs: one based on a non-standard semantics of HOL (ITP'15), and a proof-theoretic one (ESOP'17). Our most recent result (POPL'18) improves on these results by establishing the stronger properties of meta-safety and conservativity. We have also proposed (and proved consistent) an extension of Isabelle/HOL with local type definitions (ITP'16) improving on the traditional HOL typedef.

● I have a long-lasting interest in Gödel's incompleteness theorems. These theorems are acknowledged as having a wide scope, but this scope still remains largely unexplored on a formal basis. In recent work with Dmitriy Traytel, I formalized in Isabelle general versions of the theorems (CADE'19 and JAR 2021), and instantiated them to improve on Larry Paulson's previous result.

● Another line of research where I invest a lot of my enthusiasm is the mechanical verification of information-flow security; I believe we can have systems that are both verified and usable. In this area, the results I am most proud of are two entities, named CoCon and CoSMeDis. CoCon is a realistic conference management system verified for confidentiality (CAV'14). So far, it has been used for the Tableaux 2015 and ITP 2016 conferences. I am grateful to RS3 for supporting and encouraging this research as a reference scenario. CoSMeDis is a prototype distributed social media platform (ITP'16, Security and Privacy '17) developed jointly with an industrial partner, Global Notice Board. Both systems are built around kernels that are verified not to leak confidential information. In addition, CoSMeDis has been verified following a compositional methodology: Single-node guarantees are extended to the whole distributed network - more details here.

● Jasmin, myself and collaborators have been working at designing and formalizing sound, complete and efficient translations of Isabelle's higher order logic to the first order language spoken by (fully) automated theorem provers and SMT solvers, in order to boost Isabelle's automation (ITP'12, TACAS'13, FroCoS'13). These encodings are implemented in the Sledgehammer tool, which connects Isabelle with other mythological creatures such as E, SPASS, Vampire, CVC4 and Z3. My FroCoS slides give an overview.

● In the past, I worked on fuzzy logic and abstract model theory. My joint work with Daniel Găină on general formulations of the Robinson consistency and elementary chain theorems has been included in the standard reference book on institution-independent model theory.






An incomplete list of publications and drafts (see also my DBLP and Google Scholar profiles)

On logic and formal methods

  1. Preprint Brijesh Dongol, Matt Griffin, Andrei Popescu and Jamie Wright Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities 37th IEEE Computer Security Foundations Symposium (CSF 2024)
    Accepted.

  2. Preprint Andrei Popescu Nominal Recursors as Epi-Recursors 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)
    To appear.

  3. Preprint Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe On the Complex(ity) Landscape of Checking Infinite Descent 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024)
    To appear.

  4. Preprint Artur Graczyk, Marialena Hadjikosti, Andrei Popescu A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress) In P. Herber and A. Wijs: (eds.), 18th International Conference (iFM 2023)
    LNCS 14300, 391–397, Springer

  5. Preprint Andrei Popescu, Dmitriy Traytel Admissible Types-to-PERs Relativization in Higher-Order Logic 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023)
    Proc. ACM Program. Lang. 7(POPL): 1214-1245 (2023)

  6. Preprint Andrei Popescu Rensets and Renaming-Based Recursion for Syntax with Bindings Automated Reasoning: 11th International Joint Conference (2022)

  7. Preprint Andrei Popescu, Dmitriy Traytel Distilling the Requirements of Gödel's Incompleteness Theorems with a Proof Assistant Journal of Automated Reasoning 65: 1027–1070 (2021)

  8. Preprint Andrei Popescu, Peter Lammich, Ping Hou CoCon: A Conference Management System with Verified Document Confidentiality Journal of Automated Reasoning 65(2): 321-356 (2021)

  9. Preprint Lorenzo Gheri, Andrei Popescu A Formalized General Theory of Syntax With Bindings: Extended Version Journal of Automated Reasoning 64, 641–675 (2020)

  10. Preprint Andrei Popescu, Dmitriy Traytel A Formally Verified Abstract Account of Gödel's Incompleteness Theorems In P. Fontaine (ed.), 27th International Conference on Automated Deduction (CADE) 2019
    LNCS 11716, 7442-461, Springer

  11. Preprint Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel Bindings As Bounded Natural Functors Proc. ACM Program. Lang. 3, Principles of Programming Languages (POPL) 2019
    Article No. 22, 1-22, ACM

  12. Preprint Ondrej Kuncar, Andrei Popescu From Types to Sets by Local Type Definition in Higher-Order Logic (extended version)
    Journal of Automated Reasoning 62(2): 237-260 (2019)
    (Special issue dedicated to ITP 2016)

  13. Preprint Ondrej Kuncar, Andrei Popescu A Consistent Foundation for Isabelle/HOL (extended version, including detailed proofs)
    Journal of Automated Reasoning 62(4): 531-555 (2019)
    (Special issue dedicated to ITP 2015)

  14. Preprint Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi CoSMed: A Confidentiality-Verified Social Media Platform (extended version) Journal of Automated Reasoning 61(1-4): 113-139 (2018)
    (Special issue on Milestones in Interactive Thoerem Proving, dedicated to Tobias Nipkow's 60th birthday)

  15. Preprint Ondřej Kunčar, Andrei Popescu Safety and conservativity of definitions in HOL and Isabelle/HOL Proc. ACM Program. Lang. 2, Principles of Programming Languages (POPL) 2018,
    Article No. 24, 1-24, ACM

  16. Preprint Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel Foundational nonuniform (co)datatypes for higher-order logic In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017,
    1-12, ACM / IEEE

  17. Preprint Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees In 38th IEEE Symposium on Security and Privacy (S&P) 2017
    729-748, IEEE

  18. Preprint Ondřej Kunčar, Andrei Popescu Comprehending Isabelle/HOL's consistency In H. Yang (ed.), 26th European Symposium on Programming (ESOP) 2017,
    LNCS 10201, 724-749, Springer

    Here are the slides of my two end-to-end ESOP 2017 talks.

  19. Preprint Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel Friends with benefits: Implementing corecursion in foundational proof assistants In H. Yang (ed.), 26th European Symposium on Programming (ESOP) 2017,
    LNCS 10201, 111-140, Springer

  20. Preprint Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Soundness and completeness proofs by coinductive methods Journal of Automated Reasoning 58(1): 149-179 (2017) (Special issue dedicated to IJCAR 2014)

  21. Preprint Lorenzo Gheri, Andrei Popescu A Formalized General Theory of Syntax With Bindings In M. Ayala- Rincón and C. A. Muñoz (eds.), 8th International Conference on Interactive Theorem Proving (ITP) 2017
    LNCS 10499, 241-261, Springer

  22. Preprint Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone Encoding monomorphic and polymorphic types Logical Methods in Computer Science 12(4), 2016 (Special issue dedicated to TACAS 2013)

  23. Preprint Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi CoSMed: A Confidentiality-Verified Social Media Platform In J. C. Blanchette and S. Merz (eds.), 7th International Conference on Interactive Theorem Proving (ITP) 2016,
    LNCS 9807, 87-106, Springer

  24. Preprint Ondřej Kunčar, Andrei Popescu From Types to Sets by Local Type Definitions in Higher-Order Logic In J. C. Blanchette and S. Merz (eds.), 7th International Conference on Interactive Theorem Proving (ITP) 2016,
    LNCS 9807, 200-218, Springer

  25. Preprint Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Foundational Extensible Corecursion: A Proof Assistant Perspective In K. Fisher and J. H. Reppy (eds.), 20th ACM SIGPLAN International Conference on Functional Programming (ICFP) 2015,
    192-204, ACM

  26. Preprint Slides Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Witnessing (Co)datatypes In J. Vitek (ed.), 24th European Symposium on Programming (ESOP) 2015
    LNCS 9032, 359-382, Springer

  27. Preprint Andrei Popescu, Grigore Roșu Term-Generic Logic Theoretical Computer Science 577: 1–24 (2015)

  28. Preprint Ondřej Kunčar, Andrei Popescu A Consistent Foundation for Isabelle/HOL In C. Urban and X. Zhang (eds.), 6th International Conference on Interactive Theorem Proving (ITP) 2015,
    LNCS 9236, 234-252, Springer

  29. Preprint Slides Sudeep Kanav, Peter Lammich, Andrei Popescu A Conference Management System with Verified Document Confidentiality In A. Biere and R. Bloem (eds.), 26th International Conference on Computer Aided Verification (CAV) 2014,
    LNCS 8559, 167-183, Springer

  30. Preprint Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel Truly Modular (Co)datatypes for Isabelle/HOL In G. Klein and R. Gamboa (eds.), 5th International Conference on Interactive Theorem Proving (ITP) 2014,
    LNCS 8558, 93-110, Springer

  31. Preprint Slides Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Cardinals in Isabelle/HOL In G. Klein and R. Gamboa (eds.), 5th International Conference on Interactive Theorem Proving (ITP) 2014,
    LNCS 8558, 111-127, Springer

  32. Preprint Tobias Nipkow, Andrei Popescu Making Security Type Systems Less Ad Hoc it - Information Technology 56(6): 267-272 (2014)

  33. Preprint Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Unified Classical Logic Completeness: A Coinductive Pearl In S. Demri, D. Kapur and C. Weidenbach (eds.), 7th International Joint Conference on Automated Reasoning (IJCAR) 2014
    LNCS 8562, 46-60, Springer

  34. Preprint Slides Andreas Schropp, Andrei Popescu Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory In G. Gonthier and M. Norrish (eds.), 3rd International Conference on Certified Programs and Proofs (CPP) 2013,
    LNCS 8307, 114-130, Springer

  35. Preprint Slides Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formalizing Probabilistic Noninterference In G. Gonthier and M. Norrish (eds.), 3rd International Conference on Certified Programs and Proofs (CPP) 2013,
    LNCS 8307, 259-275, Springer

  36. Preprint Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formal Verification of Language-Based Concurrent Noninterference Journal of Formalized Reasoning 6(1), 2013

  37. Preprint Slides Jasmin Christian Blanchette, Andrei Popescu Mechanizing the metatheory of Sledgehammer In P. Fontaine, C. Ringeissen and R. A. Schmidt (eds.), 9th International Symposium on Frontiers of Combining Systems (FroCoS) 2013
    LNCS 8152, 245-260, Springer

  38. Preprint Slides Andrei Popescu, Johannes Hölzl, Tobias Nipkow Noninterfering Schedulers: When Possibilistic Noninterference Implies Probabilistic Noninterference In In R. Heckel and S. Milius (eds.), 5th International Conference on Algebra and Coalgebra in Computer Science (CALCO) 2013,
    LNCS 8089, 236-252, Springer

  39. Preprint Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone Encoding Monomorphic and Polymorphic Types In N. Piterman and S. A. Smolka (eds.), 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2013
    LNCS 7795, 493-507, Springer

  40. Preprint Andrei Popescu, Johannes Hölzl, Tobias Nipkow Proving Concurrent Noninterference In C. Hawblitzel and D. Miller (eds.), 2nd International Conference on Certified Programs and Proofs (CPP) 2012
    LNCS 7795, 109-125, Springer
    Receiver of the RS3 best paper award for 2012-2013

  41. Preprint Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification In L. Beringer and A. P. Felty (eds.), 3rd Conference on Interactive Theorem Proving (ITP) 2012
    LNCS 7406, 345-360, Springer

  42. Preprint Slides Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving LICS 2012
    596-605, IEEE

  43. Preprint Andrei Popescu, Elsa L. Gunter Recursion principles for syntax with bindings and substitution In M. M. T. Chakravarty, Z. Hu and O. Danvy (eds.), 16th ACM SIGPLAN International Conference on Functional Programming (ICFP) 2011
    346-358, ACM

  44. Preprint Slides Slides Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn Strong Normalization for System F by HOAS on Top of FOAS LICS 2010
    31-40, IEEE

  45. Preprint Slides Andrei Popescu, Elsa L. Gunter Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization In C.-H. L. Ong (ed.), 13th International Conference on Foundations of Software and Computational Structures (FoSSaCS) 2010
    LNCS 6014, 109-127, Springer

  46. Preprint Andrei Popescu, Traian Florin Șerbănuță, Grigore Roșu A semantic approach to interpolation Theoretical Computer Science 410(12-13): 1109-1128 (2009)

  47. Preprint Slides Andrei Popescu Weak Bisimilarity Coalgebraically In A. Kurz, M. Lenisa and A. Tarlecki (eds.), 3rd International Conference on Algebra and Coalgebra in Computer Science (CALCO) 2009
    LNCS 5728, 157-172, Springer

  48. Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu Theory support for weak higher order abstract syntax in Isabelle/HOL In J. Cheney and A. P. Felty (eds.), 4th International Workshop on Logical Frameworks and Meta- Languages: Theory and Practice, 2009
    12-20, ACM

  49. Preprint Andrei Popescu, Grigore Roșu Term-Generic Logic. In A. Corradini and U. Montanari (eds.), 19th International Workshop on Algebraic Development Techniques (WADT) 2008
    LNCS 5486, 290-307, Springer

  50. Daniel Găină, Andrei Popescu An Institution-Independent Proof of the Robinson Consistency Theorem Studia Logica 85(1): 41-73 (2007)

  51. Daniel Găină, Andrei Popescu An Institution-independent Generalization of Tarski's Elementary Chain Theorem Journal of Logic and Computation 16(6): 713-735 (2006)

  52. Andrei Popescu, Traian Florin Șerbănuță, Grigore Roșu A Semantic Approach to Interpolation In L. Aceto and A. Ingólfsdóttir (eds.), 9th International Conference on Foundations of Software Science and Computation Structure (FoSSaCS) 2006
    LNCS 3921, 307-321, Springer

  53. Preprint Andrei Popescu, Grigore Roșu Behavioral Extensions of Institutions In J. L. Fiadeiro, N. Harman, M. Roggenbach and J. J. M. M. Rutten (eds.), 1st International Conference on Algebra and Coalgebra in Computer Science (CALCO) 2005
    LNCS 3629, 331-347, Springer

  54. Andrei Popescu Languages Generated Using an Abstract Catenation Grammars 7: 31-40 (2004)

On fuzzy logic and algebra

  1. Andrei Popescu Some algebraic theory for many-valued relation algebras Algebra Universalis 56: 211-235 (2007)

  2. George Georgescu, Andrei Popescu A common generalization for MV-algebras and Lukasiewicz-Moisil algebras Archive for Mathematical Logic 45(8): 947-981 (2006)

  3. George Georgescu, Ioana Leustean, Andrei Popescu Order convergence and distance on Lukasiewicz-Moisil algebras Journal of Multiple-Valued Logic and Soft Computing 12(1-2): 33-69 (2006)

  4. George Georgescu, Andrei Popescu A new class of probabilities on Lukasiewicz-Moisil algebras Journal of Multiple-Valued Logic and Soft Computing 12(3-4): 337-354 (2006)

  5. George Georgescu, Andrei Popescu Similarity Convergence in Residuated Structures Logic Journal of the IGPL 13(4): 389-413 (2005)

  6. Andrei Popescu Lukasiewicz-Moisil Relation Algebras Studia Logica 81(2): 167-189 (2005)

  7. Andrei Popescu Many-Valued Relation Algebras Algebra Universalis 53: 73-108 (2005)

  8. George Georgescu, Andrei Popescu Non-dual fuzzy connections Archive for Mathematical Logic 43(8): 1009-1039 (2004)

  9. George Georgescu, Andrei Popescu Non-commutative fuzzy structures and pairs of weak negations Fuzzy Sets and Systems 143(1): 129-155 (2004)

  10. Andrei Popescu A general approach to fuzzy concepts Mathematical Logic Quarterly 50(3): 265-280 (2004)

  11. George Georgescu, Andrei Popescu Non-commutative fuzzy Galois connections Soft Computing 7(7): 458-467 (2003)

  12. George Georgescu, Andrei Popescu Concept lattices and similarity in non-commutative fuzzy logic Fundamenta Informaticae 53(1): 23-54 (2002)





Ph.D. theses

  1. Preprint   Contributions to the Theory of Syntax with Bindings and to Process Algebra University of Illinois at Urbana-Champaign (2010)
    Advisor: Elsa Gunter

  2.  Many-Valued Relation Algebra University of Bucharest (2005)
    Advisor: George Georgescu





Edited volumes

  1. Andrei Popescu and Steve Zdancewic (eds.) Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022) — Philadelphia, PA, USA, January 17-18, 2022. ACM 2022, ISBN 978-1-4503-9182-5

  2. Cătălin Hrițcu and Andrei Popescu (eds.) Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021) — Virtual Event, Denmark, January 17-19, 2021. ACM 2021, ISBN 978-1-4503-8299-1

  3. Andreas Herzig and Andrei Popescu (eds.) Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS 2019) — London, UK, September 4-6, 2019. LNCS 11715, Springer

  4. Serenella Cerrito and Andrei Popescu (eds.) Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019) — London, UK, September 3-5, 2019. LNCS 11714, Springer





Isabelle Developments in The Archive of Formal Proofs

  1. Andrei Popescu, Peter Lammich Bounded-Deducibility Security Archive of Formal Proofs (2014)

  2. Markus N. Rabe, Peter Lammich, Andrei Popescu A shallow embedding of HyperCTL* Archive of Formal Proofs (2014)

  3. Andrei Popescu, Johannes Hölzl Probabilistic Noninterference Archive of Formal Proofs (2014)

  4. Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Abstract Completeness Archive of Formal Proofs (2014)

  5. Jasmin Christian Blanchette, Andrei Popescu Sound and Complete Sort Encodings for First-Order Logic Archive of Formal Proofs (2013)

  6. Andrei Popescu, Johannes Hölzl Possibilistic Noninterference Archive of Formal Proofs (2012)

  7. Andrei Popescu Ordinals and Cardinals Archive of Formal Proofs (2009)