Catalin is a tenured Research Scientist at Inria Paris where he develops rigorous formal techniques for solving security problems. He is particularly interested in formal methods for security (memory safety, compartmentalization, dynamic monitoring, integrity, security protocols, information flow), programming languages (type systems, verification, proof assistants, property-based testing, semantics, formal metatheory, certified tools), and the design and verification of security-critical systems (reference monitors, secure compilers, microkernels, secure hardware). He is a developer of the new F* verification system and of several other open source tools based on his research. Catalin was a PhD student at Saarland University and a Research Associate at University of Pennsylvania before joining Inria Paris in September 2013.