Cătălin Hrițcu

Formally Verified Security

Cătălin Hrițcu is a tenured faculty member and head of the Formally Verified Security group at the MPI-SP. He is particularly interested in formal methods for security (secure compilation, compartmentalization, memory safety, security protocols, information flow), programming languages (program verification, proof assistants, dependent types, formal semantics, mechanized metatheory, property-based testing), and the design and verification of security-critical systems (reference monitors, secure compilation chains, tagged architectures).

Cătălin was awarded an ERC Starting Grant on formally secure compilation, and is also actively involved in the design of the F* verification system, which is used for building a formally verified HTTPS stack. Cătălin received a PhD from Saarland University, a Habilitation from ENS Paris, and was previously also a Tenured Researcher at Inria Paris, a Postdoctoral Research Associate at University of Pennsylvania, and a Visiting Researcher at Microsoft Research Redmond.

Formally Verified Security Group

Cezar Andrici
Roberto Blanco
Jérémy Thibault

Former Members

Carmine Abate
Adrien Durier
Théo Winterhalter
Maxi Wuttke
Go to Editor View