Cătălin Hrițcu
Tenured faculty and head of the Formally Verified Security group
at the
Max Planck Institute for Security and Privacy (MPI-SP)
in Bochum, Germany.
I am also Adjunct Professor (APL) in the Faculty of Computer Science
of Ruhr University Bochum (RUB)
and PI
of the CASA Cluster of Excellence at RUB.
Between October 2013 and April 2020 I was a
tenured researcher (chargé de recherche)
at Inria Paris
in the Prosecco team.
Between May 2011 and
September 2013 I was a Postdoctoral Research Associate at
the University of Pennsylvania,
working under the supervision
of Benjamin
C. Pierce.
In the fall of 2016 I held a Visiting Researcher position at
Microsoft Research Redmond.
I received my PhD
from Saarland
University in Saarbrücken, Germany
and also a Habilitation from ENS Paris.
Quick Links:
Contact;
Interests;
Group;
Publications;
Talks;
Teaching;
Tools;
Misc
Recent Research Projects
News/Events
-
IEEE Symposium on Security and Privacy
(Associate PC Chair in 2026,
also PC Member in 2020)
- IEEE SP 2026 abstract deadlines: 29 May 2025 and 6 November 2025
- IEEE SP 2026 submission deadlines: 5 June 2025 and 13 November 2025
- IEEE SP 2026 symposium: 18-21 May 2026 in San Francisco
- Roberto "Rob" Blanco, previously PostDoc in my group, started as Associate Professor at TU Eindhoven in May 2025.
-
International Conference on Functional Programming, ICFP
(PC Member in 2025)
- ICFP 2025 conference: 12-18 October 2025, Singapore
(co-located with SPLASH)
- Zoe Paraskevopoulou,
former MSc intern in my group and longer-term collaborator, took an Assistant Professor position at
the National Technical University of Athens in September 2024.
- Certified Programs and Proofs, CPP (Steering Committee Chair since 2021;
also PC Chair and Conference Chair in 2020 and 2021; also PC member in 2016)
- CPP 2026 conference: 11-17 January 2026, Rennes, France (with POPL)
-
Computer and Communications Security, CCS
(Track PC Chair for Formal Methods and Programming Languages in 2024,
also PC Member in 2018)
- Computer Security Foundations, CSF (Steering Committee Member since 2024, Test-of-Time Awards Chair in 2023 and 2024; also PC Member in 2020, 2021 and 2024)
- CSF 2025: June 16-20, 2025 - Santa Cruz, CA, USA
- Principles of Secure Compilation, PriSC (Steering Committee Chair 2019--2023, Steering Committee Member since 2023, also PC Chair in 2018)
-
Transactions on Privacy and Security, TOPS (Editor since May 2024)
- Danel Ahman, former PostDoc in my group, started as Associate Professor at University of Tartu in January 2024.
- Adrien Durier, former PostDoc in my group, started as Associate Professor (Maître de Conférences) at Université Paris-Saclay and LMF in September 2023.
- Théo Winterhalter, former PostDoc in my group, took a tenured researcher position (CR) at Inria Saclay, in Deducteam, starting in October 2022. Kenji Mailard, graduated PhD student I supervised, has obtained a similar Inria position (ISFP), in the Gallinette team in Nantes.
- Arthur Azevedo de Amorim, graduated PhD student I co-supervised at University of Pennsylvania, started as Assistant Prof. at Rochester Institute of Technology in Jan 2023.
- Guido Martínez, co-supervised student at CIFASIS-CONICET and UNR, Argentina, started as a Research Software Engineer at Microsoft Research in Redmond in Jan 2023.
-
Principles of Programming Languages, POPL
(Artifact Evaluation Chair in 2018 and 2019;
also PC Member in 2017 and 2024)
- POPL 2026 submission deadline: 10 July 2025
- POPL 2026 symposium: 11-17 January 2026, Rennes, France
E-mail: catalin.hritcu@gmail.com or catalin.hritcu@mpi-sp.org
Address:
Universitätsstraße 142, 44799 Bochum, Germany
On the RUB Campus, Building: MB (aka TZR), Floor 1, Office: S-W 106
Research Interests
My research is primarily focused on developing rigorous formal
techniques for solving security problems. I am
particularly interested in:
-
formal methods for computer security:
memory safety,
compartmentalization,
dynamic monitoring,
integrity
-
programming-languages techniques:
type systems,
program verification,
proof assistants,
property-based testing,
semantics,
formal metatheory,
certified tools
-
design and verification of security-critical systems:
reference monitors,
secure compilation chains,
secure hardware
Formally Verified Security Research Group
I am very fortunate to work with a group of outstanding students and starting researchers:
For a complete list of past members of my group please look here.
Recent Publications and Drafts
For a complete list of my papers please look here
(also on DBLP and Google Scholar).
-
Jérémy Thibault,
Joseph Lenormand, and
Cătălin Hrițcu.
Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs.
Submitted to ITP'25. Draft from March 2025.
-
Cezar-Constantin Andrici,
Danel Ahman,
Cătălin Hrițcu,
Ruxandra Icleanu,
Guido Martínez
Exequiel Rivas, and
Théo Winterhalter.
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*.
Submitted to ICFP'25. Draft from February 2025.
-
Jonathan Baumann,
Roberto Blanco,
Léon Ducruet,
Sebastian Harwig, and
Cătălin Hrițcu.
FSLH: Flexible Mechanized Speculative Load Hardening.
In 38th IEEE Computer Security Foundations Symposium (CSF).
June 2025.
-
Jérémy Thibault,
Roberto Blanco,
Dongjae Lee,
Sven Argo,
Arthur Azevedo de Amorim,
Aïna Linn Georges,
Cătălin Hrițcu, and
Andrew Tolmach.
SECOMP: Formally Secure Compilation of Compartmentalized C Programs.
In 31th ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 1061–1075. ACM, October 2024.
-
Cezar-Constantin Andrici,
Ștefan Ciobâcă,
Cătălin Hrițcu,
Guido Martínez,
Exequiel Rivas,
Éric Tanter, and
Théo Winterhalter.
Securing Verified IO Programs Against Unverified Code in F*.
PACMPL, 8(POPL):74:1--74:34, January 2024.
-
Roberto Blanco,
Christian Doczkal,
Jakob Feldtkeller,
Tim Güneysu, and
Cătălin Hrițcu.
Short Paper: Mechanized Proofs of Masking Security.
18th Workshop on Programming Languages and Analysis for Security (PLAS 2023 at
CCS 2023).
November 2023.
-
Philipp G. Haselwarter,
Benjamin Salling Hvass,
Lasse Letager Hansen,
Théo Winterhalter,
Cătălin Hrițcu, and
Bas Spitters.
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
In 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 30–44. ACM, January 2024.
-
Philipp G. Haselwarter,
Exequiel Rivas,
Antoine Van Muylder,
Théo Winterhalter,
Carmine Abate,
Nikolaj Sidorenco,
Cătălin Hrițcu,
Kenji Maillard, and
Bas Spitters.
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
In ACM Transactions on Programming Languages and Systems (TOPLAS).
Volume 45, Issue 3, July 2023.
-
Cezar-Constantin Andrici,
Théo Winterhalter,
Cătălin Hrițcu, and
Exequiel Rivas.
Verifying non-terminating programs with IO in F*.
Presentation at the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2022).
September 2022.
-
Théo Winterhalter,
Cezar-Constantin Andrici,
Cătălin Hrițcu,
Kenji Maillard,
Guido Martínez, and
Exequiel Rivas.
Partial Dijkstra Monads for All.
Extended abstract of presentation at the 28th International Conference on Types for Proofs and Programs (TYPES 2022).
June 2022.
-
Akram El-Korashy,
Roberto Blanco,
Jérémy Thibault,
Adrien Durier,
Deepak Garg, and
Cătălin Hrițcu.
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation.
In 35th
IEEE Computer Security Foundations Symposium (CSF).
August 2022.
-
Maximilian Algehed,
Jean-Philippe Bernardy, and
Cătălin Hrițcu.
Dynamic IFC Theorems for Free!
In 34nd
IEEE Computer Security Foundations Symposium (CSF), pages 1--14. June 2021.
-
Carmine Abate,
Roberto Blanco,
Ștefan Ciobâcă,
Adrien Durier,
Deepak Garg,
Cătălin Hrițcu,
Marco Patrignani,
Éric Tanter, and
Jérémy Thibault.
Trace-Relating Compiler Correctness and Secure Compilation.
In 29th European Symposium on Programming (ESOP), pages 1--28. Springer, April 2020.
Nominated for EATCS Award for the best ETAPS 2020 paper in theoretical computer science.
-
Kenji Maillard,
Cătălin Hrițcu,
Exequiel Rivas, and
Antoine Van Muylder.
The Next 700 Relational Program Logics.
PACMPL, 4(POPL):4:1--4:33, January 2020.
-
Kenji Maillard,
Danel Ahman,
Robert Atkey,
Guido Martínez,
Cătălin Hrițcu,
Exequiel Rivas, and
Éric Tanter.
Dijkstra Monads for All.
PACMPL, 3(ICFP):104:1– 104:29, August 2019.
-
Carmine Abate,
Roberto Blanco,
Deepak Garg,
Cătălin Hrițcu,
Marco Patrignani, and
Jérémy Thibault.
Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation.
In 32nd
IEEE Computer Security Foundations Symposium (CSF), pages 256--271. June 2019.
Distinguished Paper Award.
Talks
Here are my recent and upcoming talks. For a complete list of my talks please look here.
- My Group's Journey in Secure Compilation
- SECOMP: Formally Secure Compilation of Compartmentalized C Programs
- Short teaser for our courses at Ruhr Uni Bochum
- Formally Verified Security
- Certified Programs and Proofs, CPP
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- The Next 700 Relational Program Logics
- Everest All Hands: slides (2019-10-11)
- Dijkstra Monads for All
- Everest All Hands: slides (2019-10-10)
- When Good Components Go Bad
Teaching
Co-author of 3 volumes of the Software Foundations textbook:
Logical Foundations,
Programming Language Foundations, and
Security Foundations (draft, main author).
Here are my recent courses. For a complete list of my teaching please look here.
- Ongoing: Foundations of Programming Languages, Verification, and Security course at Ruhr Uni Bochum, April--July 2025
- Recent: Proofs are Programs course at Ruhr Uni Bochum, October 2024--February 2025
- Recent: Functional Programming course at Ruhr Uni Bochum, April--July 2024
- Foundations of Programming Languages, Verification, and Security course at Ruhr Uni Bochum, October 2023--February 2024
- Proofs are Programs course at Ruhr University Bochum, April--July 2023
- Writing and Verifying Functional Programs in Coq course at
Summer School on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019,
24-31 August 2019 at INSA, Lyon, France
- Program Verification with F* course at Summer School on
Verification Technology, Systems, and Applications, VSTA 2019,
1-5 July 2019 at University of Luxembourg
- Formally Secure Compartmentalizing Compilation course at
International School on Foundations of Security Analysis and Design (FOSAD),
27-28 August, 2018, Bertinoro, Italy
- Program Verification with F* course at
EPIT 2018 Software Verification Spring School, 7-11 May, 2018, Aussois, France
Here are my current software projects. For a complete list of software please look here.
Misc
