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 was also involved in the design of the F* verification system, which was 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

Name
Cezar Andrici
Roberto Blanco
Jérémy Thibault

Former Members

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