PhD in Computer Science from University of Champaign-Urbana at Illinois, US
Ms and BA in Computer Science from University of Bucharest, Romania
I am interested in Software Verification, Theorem Proving, Inductive and Coinductive Datatypes, Security.
I am a co-designer of Isabelle/ HOL's new inductive and coinductive datatype package and of CoCon, an EasyChair-like conference management system verified for confidentiality.
More information can be found on my webpage.
Gheri, Lorenzo and Popescu, Andrei (2017) A formalized general theory of syntax with bindings. In: 8th International Conference Interactive Theorem Proving (ITP), 26-29 Sept 2017, University of Brasília, Brazil. (Accepted/In press)
Blanchette, Jasmin Christian and Meier, Fabian and Popescu, Andrei and Traytel, Dmitriy (2017) Foundational nonuniform (co)datatypes for higher-order logic. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 20-23 Jun 2017, Reykjavik, Iceland.
Bauereiß, Thomas and Pesenti Gritti, Armando and Popescu, Andrei and Raimondi, Franco (2017) CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. In: 38th IEEE Symposium on Security and Privacy, 22-26 May 2017, San Jose, CA, USA.
Blanchette, Jasmin Christian and Bouzy, Aymeric and Lochbihler, Andreas and Popescu, Andrei and Traytel, Dmitriy (2017) Friends with benefits: implementing corecursion in foundational proof assistants. In: 26th European Symposium on Programming, ESOP 2017, 22-29 Apr 2017, Uppsala, Sweden.
Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy (2017) Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58 (1). pp. 149-179. ISSN 0168-7433