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. (Accepted/In press)
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
Principal investigator for EPSRC first-grant EP/N019547/1. Project: Verification of Web-based Systems (VOWS). Website: http://gtr.rcuk.ac.uk/projects?ref=EP/N019547/1 Grant value: 100,933 GBP. Starting time: March 2016. Duration: 2 years.
Funded researcher (2010–2013) and project partner (2014–2015) for DFG grant Ni 491/13. Project title: Security type systems and deduction (PI: Tobias Nipkow). Website: http://www21.in.tum.de/~popescua/rs3/secded.html Grant value: 600,000 Euro. Starting time: Oct. 2010. Duration: 6 years.
Program Committee Membership
Interactive Theorem Proving (ITP) 2016
International Joint Conference on Automated Reasoning (IJCAR) 2016
The 5th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP) 2016
The 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) 2015
The 8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: Theory & Practice (LFMTP) 2013
Prizes and Awards
Best Paper Award for 2012/2013 within the Reliably Secure Software Systems (RS3), a priority program funded by the German Research Foundation (DFG), encompassing 12 main projects and 6 associated projects. This was for the paper 'Proving Concurrent Noninterference' (published in CPP 2012), coauthored with Johannes Holzl and Tobias Nipkow
Saburo Muroga Fellowship for outstanding CS graduate students 2005, offered by the Department of Computer Science, UIUC
Mavis Memorial Fund Scholarship Award 2006, offered by the College of Engineering, UIUC
Technical Institute Munich, Germany: Tobias Nipkow's group
University of Illinois at Urbana-Champaign, US: Grigore Rosu's group, Elsa Gunter's group
Inria & LORIA, Nancy, France: Jasmin Blanchette
Japan Advanced Institute of Science and Technology, Kyoto, Japan: Daniel Gaina.