معرفی
Andrei Popescu is a Senior Lecturer in Computing Foundations at the School of Computer Science, University of Sheffield, where he also serves as School Programmes Lead (PGT). He is a member of both the Security of Advanced Systems research group and the Foundations of Computation research group. Prior to joining Sheffield in May 2020, he was a Lecturer at Middlesex University and a postdoctoral researcher at TU Munich.
Dr. Popescu holds dual PhDs: one in computer science from the University of Illinois at Urbana-Champaign (advised by Elsa L. Gunter and Grigore Roșu) and another in mathematics from the University of Bucharest (advised by George Georgescu).
His primary research interests include proof assistants, information flow security, inductive and coinductive datatypes, automated deduction, and syntax with bindings. His work often focuses on the formal verification of security properties in practical systems, as evidenced by projects like CoCon (a conference management system with verified confidentiality) and CoSMeDis (a social media platform with formally verified security guarantees).
Analysis of his recent publications reveals a strong focus on foundational aspects of proof assistants, particularly Isabelle/HOL, with significant contributions to syntax with bindings, recursion principles, and the formalization of Gödel's incompleteness theorems. His work bridges theoretical computer science with practical applications in security verification.
Scientific Awards:
- Distinguished paper award at POPL 2025 for 'Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings'
- Distinguished paper award at POPL 2024 for 'Nominal Recursors as Epi-Recursors'
- Distinguished paper award at POPL 2023 for 'Admissible Types-to-PERs Relativization in Higher-Order Logic'
Dr. Popescu has successfully supervised PhD students, including Lorenzo Gheri whose thesis focused on syntax with bindings. He has secured significant research funding, including the COVERT project (EPSRC, £422,585), Security of Digital Twins in Manufacturing (EPSRC, £774,954), and Cyclic Reasoning Mechanisms for Interactive Theorem Proving (Royal Society, £12,000).
He is actively involved in the research community, serving on program committees for major conferences including POPL, ITP, CSF, and IJCAR, and co-organizing the Midlands Graduate School. His work with the Security of Advanced Systems group continues to advance the field of formal verification for security-critical systems.
