Cătălin Hriţcu

Registered user since Wed 27 May 2015

Name: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 new Max Planck Institute for Security and Privacy (MPI-SP) in Bochum, Germany. 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). He 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. Catalin 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.

Research interests:Formal methods for security


PriSC 2023 Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces
Session Chair of Session 2 (part of PriSC 2023)
SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
Steering Committee Chair in Steering Committee within the PriSC 2023-track
CPP 2023 Steering Committee Chair in Steering Committee within the CPP 2023-track
Show activities from other conferences

POPL 2023-profile
View general profile