Cătălin Hriţcu

Software

ERC SECOMP: Efficient Formally Secure Compilation
F*: From Program Verification System to Proof Assistant (with Nikhil Swamy, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthik Bhargavan, Cédric Fournet, and others)
Luck: A Domain Specific Language For Property-Based Generators (with Leonidas Lampropoulos, Li-yao Xia, Benjamin C. Pierce, John Hughes, and Zoe Paraskevopoulou)
QuickChick: Property-based testing plugin for Coq, including a foundational verification framework for testing code (with Maxime Dénès, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce)
Micro-Policies: Formally Verified, Tag-Based Security Monitors (with Arthur Azevedo de Amorim, André DeHon, Maxime Dénès, Udit Dhawan, Nick Giannarakis, Yannis Juglaret, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach)
CRASH/SAFE: clean-slate co-design of a secure architecture, including novel hardware, operating system, and programming language (~40 people team)
Breeze: a programming language with dynamic information flow control and label-based access control (with Michael Greenberg, Ben Karel, Benoît Montagu, Greg Morrisett, Benjamin C. Pierce, Jesse A. Tov, and others)
F5: a tool-chain for RCF (with Thorsten Tarrach)
DVerify: a verification tool for the Dminor language (by Thorsten Tarrach)
Dminor: a type-checker using semantic subtyping (with Gavin Bierman and Andy Gordon)
Expi2Java: an extensible code generator for security protocols (by Alex Busenius)
Protocol transformation for achieving security despite compromise (by Martin Grochulla)
Zero-knowledge type-checker (with Stefan Lorenz, Kim Pecina and Thorsten Tarrach)