Cătălin Hriţcu

Software

SECOMP: Secure Compilation Chain for Compartmentalized C Programs (with Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, and Andrew Tolmach)
F*: Program Verification System for Effectful Programs (with Nikhil Swamy, Guido Martínez, Aseem Rastogi, Tahina Ramananandro, and others)
SSProve: A foundational framework for modular cryptographic proofs in Coq (with Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Kenji Maillard, and Bas Spitters, and others)
QuickChick: Property-based testing plugin for Coq, including a foundational verification framework for testing code (with Leonidas Lampropoulos, Maxime Dénès, Zoe Paraskevopoulou, Benjamin C. Pierce, 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)
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)