Cătălin Hrițcu
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.