back to home page

Cătălin Hriţcu

Current Research Group on Formally Verified Security

• Cezar-Constantin Andrici
  • PhD Student at MPI-SP, since 2021-10:
    Towards the secure interoperability between F* and ML
  • Research Intern/Engineer at MPI-SP, 2020-07 to 2020-11:
    Towards the secure interoperability between F* and ML
    
    [1st prize at Student Research Competition of ICFP 2020 (graduates section)]
  • Research Intern/Engineer at Inria Paris, 2019-07 to 2019-11:
    Verifying programs with IO in F* including a simple web server
  [MSc student at University of Iasi, Romania] [PhD student at MPI-SP/RUB]
• Jonathan Baumann
  • PhD Student at MPI-SP, since 2025-10:
    Formally Secure Compilation against Spectre Attacks
  • Research Intern at MPI-SP, 2020-04 to 2020-09:
    FSLH: Flexible Mechanized Speculative Load Hardening
  [MSc student at ENS Paris-Saclay] [PhD student at MPI-SP/RUB]
• Yonghyun Kim
• Postdoctoral Researcher at MPI-SP, since 2025-05:
  Formally Secure Compilation against Spectre Attacks
• Julay Leatherman-Brooks (Research Intern, Portland State University)
• Abigail Pribisova (Research Immersion Lab, cs@max planck student)
• Jérémy Thibault
  • Visitor at MPI-SP, since 2025-09
  • Graduated PhD Student at Inria Paris (2018-08 to 2020-04) then at MPI-SP (2020-05 to 2025-08): Scalable Proof Techniques for Formally Secure Compilation of Compartmentalized Programs
  • Research Intern at Inria Paris 2018-02 to 2018-07:
    A Trace-based Proof Technique for Secure Compilation
  [MSc student at ENS Rennes] [PhD student at Inria/ENS Paris, then at MPI-SP/RUB] [Now PostDoc at EPFL]

Past Group Members

• Roberto Blanco
  • Postdoctoral Researcher at MPI-SP, 2020-05 to 2025-04
    Formally Secure Compilation and Formal Methods for Side-Channel Secure Hardware
  • Starting Researcher Position at Inria Paris, 2018-01 to 2020-04:
    Formally Secure Compilation Despite Dynamic Compromise
  [Started as Associate Professor at TU Eindhoven in May 2025]
• Basile Schlosser
  • Research Intern at MPI-SP, 2025-02 to 2025-06:
    Formally Secure Compilation to the Micro-Policies Tagged Architecture
  [MSc Student at ENS Paris-Saclay]
• Léon Ducruet
  • Research Intern at MPI-SP, 2024-10 to 2025-02:
    FSLH: Flexible Mechanized Speculative Load Hardening
  [MSc Student at ENS Lyon] [Now intern at Aarhus University]
• Sebastian Harwig
  • Teaching Assistant Student at RUB and MPI-SP, 2024-10 to 2025-03:
    Proofs are Programs course at RUB.
  • Research Assistant Student at MPI-SP, 2024-04 to 2024-09
    Rocq speculative constant time and relative security proofs
  [MSc Student at RUB]
• Ruxandra Icleanu
  • Research Intern at MPI-SP, 2024-06 to 2024-09:
    Security against Unverified Stateful Code in F*
  [BSc then MSc Student at University of Edinburgh]
• Lucie Lahaye
• Research Intern at MPI-SP, 2024-05 to 2024-07:
  Property-based testing in Coq against speculative execution attacks
[MSc Student at ENS Lyon]
• Joseph Lenormand
  • Research Intern at MPI-SP, 2024-02 to 2024-06:
    Nanopass back-translation of multiple traces for secure compilation proofs
  [MSc Student at ENS Paris-Saclay]
• Maxi Wuttke
• PhD Student at MPI-SP, 2023-02 to 2024-03: Verifying probability bounds in F*
[Former PhD Student at MPI-SWS]
• Dongjae Lee
  • Research Intern at MPI-SP, 2023-03 to 2023-08: Back-Translation Proof for Formally Secure Compilation of Compartmentalized C Programs
  [MSc Student at Seoul National University, South Korea] [Now PhD Student at MIT]
• Eleftherios (Lef) Ioannidis
  • Research Intern at MPI-SP, 2023-07 to 2023-09: Verification of Distributed Systems
  [PhD Student at University of Pennsylvania][Senior Research Software Engineer at Microsoft Research]
• Guido Martínez
  • Co-Supervised PhD Student at CIFASIS-CONICET Rosario 2017-04 to 2022-12:
    The F* Language for Semi-Automatic Verification of Effectful Programs
  • Research Internship funded by MSR-Inria Joint Centre, 2018-09 to 2018-12:
    Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
  • Research Internship funded by MSR-Inria Joint Centre, 2016-01 to 2016-06:
    Dijkstra Monads for Free
  [MSc student at PhD student at National University of Rosario] [PhD student at CIFASIS-CONICET Rosario]
  [Now Research Software Engineer at Microsoft Research in Redmond]
• Carmine Abate
  • Graduated PhD student at Inria Paris (2018-06 to 2020-04) then at MPI-SP (2020-05 to 2022-04): A Formal Framework for Correct and Secure Compilation
  • Research Intern at Inria Paris, 2017-12 to 2018-05:
    Robust Property Preservation for Secure Compilation
  [MSc student at University of Trento] [PhD student at Inria/ENS Paris, then at MPI-SP/RUB]
  [Now Formal Verification Senior Researcher at the Barkhausen Institut in Dresden]
• Théo Winterhalter
• Postdoctoral Researcher at MPI-SP, 2020-10 to 2022-09:
  Formal verification in F* and Coq/SSProve
[Now tenured researcher (CR) at Inria Saclay, in Deducteam]
• Aïna Linn Georges
  • Research Intern at MPI-SP, 2022-07 to 2022-09:
    Capabilities Backend to the SECOMP Secure Compiler
  [PhD Student at Aarhus University] [Now PostDoc at MPI-SWS]
• Adrien Durier
  • PostDoctoral Researcher at Inria Paris then at MPI-SP, 2019-10 to 2021-10:
    SecurePtrs and Micro-policies backend for secure compilation
  [Then PostDoc at LMF, Université Paris-Saclay]
  [Now Maître de Conférences (Associate Professor) at Université Paris-Saclay and LMF]
• Exequiel Rivas
  • Starting Researcher Position at Inria Paris 2019-03 to 2021-02:
    The Formal Semantics and Evolution of the F* Verification System
  [Then at Marigold (working on Ligo)] [Now at Tallinn University of Technology]
• Kenji Maillard
  • Graduated PhD student at Inria Paris and ENS Paris from 2017-01 to 2019-11:
    Principles of Program Verification for Arbitrary Monadic Effects
  [Then PostDoc at Inria in Nantes and University of Chile]
  [Now on permanent Inria Starting Faculty Position in the Gallinette team, Nantes and Guest at LMU, Munich]
• Antoine Van Muylder
  • Research Intern at Inria Paris 2019-05 to 2020-04:
    The next 700 relational program logics and SSProve
  [MSc student at Paris 7 and LMFI] [Now PhD student at KU Leuven]
• Théo Laurent
  • Research Engineer at Inria Paris, 2018-07 to 2020-04: R&D work on F*
  • Research Intern at Inria Paris, 2017-03 to 2017-08:
    Micro-policies backend for secure compilation
  [MSc Student at ENS Paris and MPRI] [Now PhD student at Inria]
• Éric Tanter
  • Visiting Professor on Sabbatical: 2018-07 to 2019-02 and 2019-08 to 2019-12
  [Full Professor at University of Chile]
• Ramkumar Ramachandra
  • Research Engineer at Inria Paris, 2019-08 to 2020-07: Relational program verification
  [Then MSc student at Université Paris Cité and research apprentice at IRIF] [Now Senior Compiler Engineer at Codasip]
• Florian Groult
• Research Intern/Engineer at Inria Paris from 2018-14 to 2019-10:
  Memory Sharing for a Compartmentalizing Compiler
[MSc student at Orléans University] [Then PhD student at Université d'Orléans]
• Elizabeth Labrada (Research Intern/Visitor from 2018-10 to 2019-01)
• Victor Dumitrescu
  • Research Engineer at MSR-Inria from 2017-01 to 2018-11:
    Implementing Meta-programming and Tactics in F*
[Then Software Engineer at Nomadic Labs working on Tezos]
• Danel Ahman
  • Postdoctoral Researcher at Inria Paris from 2017-04 to 2018-09:
    Semantic Foundations for F*
[Then PostDoc at University of Ljubljana] [Now Associate Professor at University of Tartu]
• Arthur Azevedo de Amorim
  • Graduated PhD student at University of Pennsylvania; 2011-08 to 2017-10,
    Co-Supervised with Benjamin C. Pierce: A Methodology for Micro-Policies
  • Research Internship at Inria, 2014-03 to 2014-08:
    Micro-Policies: Formally Verified, Tag-Based Security Monitors
  [Then PostDoc at Carnegie Mellon University and Boston University]
  [Now Assistant Professor at Rochester Institute of Technology]
• Amal Ahmed
  • Visiting Professor on Sabbatical: 2017-09 to 2018-07
  [Full Professor & Associate Dean for Graduate Programs at Northeastern University]
• Aaron/Ariel Weiss (Visiting Researcher from Northeastern University, 2017-09 to 2018-07)
• Marco Stronati
  • PostDoctoral Researcher at Inria Paris, 2017-01 to 2017-12: Formally Secure Compilation
  [Then Developer at Nomadic Labs working on Tezos][Now Research Scientist at Matter Labs]
• Guglielmo Fachini
  • Research Engineer at Inria Paris, 2017-01 to 2017-12: Secure compilation proofs in Coq
  [Now Developer at Nozomi Networks]
• Ana Nora Evans
  • Visiting Researcher at Inria Paris, 2017-05 to 2017-08:
    Software-fault isolation backend for secure compilation
  [PhD Student at University of Virginia] [Now at Renaissance School, Charlottesville and Blue Ridge Boost]
• Clément Pit-Claudel
  • Research Intern at Inria Paris, 2017-07 to 2017-10:
    Interactive proving and effect masking in F*
  [PhD Student at MIT] [Then at Amazon AWS] [Now Assistant Professor at EPFL]
• Tomer Libal
  • Research Engineer at MSR-Inria, 2017-01 to 2017-07: Refactoring the F* type-checker
  [Then Assistant Professor at The American University of Paris]
  [Now Founder and CEO of LegAI, and PostDoc at University of Luxembourg]
• William J. Bowman
  • Research Intern at Inria Paris, 2017-10 to 2017-12:
    From Coq to Dependently Typed Assembly
  [PhD Student at Northeastern University] [Now Assistant Professor at University of British Columbia]
• Yannis Juglaret
  • PhD Student funded by DGA/Inria grant, 2015-10 to 2016-09:
    Micro-Policies: High-Assurance Hardware-Assisted Security Monitors
  • Research Internship at Inria, 2015-03 to 2015-08: Towards a Fully Abstract Compiler Using Micro-Policies -- Secure Compilation for Mutually Distrustful Components
  [Student at Paris 7 and MPRI] [Then Engineer at DGA-MI] [Then R&D Engineer at Quarkslab]
  [Now Senior Software Engineer at Mozilla]
• Boris Eng
  • Research Internship at Inria (advised by Yannis Juglaret), 2016-04 to 2016-06:
    Partial type safety using Coq
  [Student at Université Paris 7] [Then ATER at Université Sorbonne Paris Nord]
  [Now R&D Engineer at OCamlPro]
• Diane Gallois-Wong
  • Research Internship at Inria, 2016-03 to 2016-08:
    Formalising Luck: Improved Probabilistic Semantics for Property-Based Generators
  [MSc Student at ENS Paris and MPRI] [Then Intern at TrustInSoft] [Then PhD student at LRI, Université Paris-Sud] [Now Research Software Engineer at Nomadic Labs]
• Alejandro Aguirre
  • Research Internship at Inria, 2016-04 to 2016-08:
    Towards a Provably Correct Encoding from F* to SMT
  [MSc Student at Paris 7 and MPRI] [Then PhD Student at IMDEA Software Institute]
  [Now PostDoc at Aarhus University]
• Li-yao Xia
  • Research Internship at Inria, 2015-04 to 2015-08: Integrating Functional Logic Programming with Constraint Solving for Random Generation of Structured Data
  [MSc Student at ENS Paris and MPRI] [Then PhD student at University of Pennsylvania] [Then PostDoc at University of Edinburgh] [Now INRIA research engineer on Creusot]
• Simon Forest
  • Research Internship at Inria, 2015-03 to 2015-08: Micro-F* in F*
  [MSc Student at ENS Paris and MPRI] [Then MSc student at LMFI] [Then PhD Student at École Polytechnique] [Then PostDoc at Institut de Mathématiques de Marseille (I2M)] [Then PostDoc at LIS at Aix-Marseille Université]
• Zoe Paraskevopoulou
  • Research Internship at Inria, 2014-04 to 2014-09:
    QuickChick: A Coq Framework For Verified Property-Based Testing (thesis)
  [MSc Student at NTU Athens and MPRI] [Then PhD student at Princeton University]
  [Then PostDoc at Northeastern University] [Now Assistant Professor at National Technical University of Athens and Formal Verification Researcher at Ethereum Foundation]
• Nick Giannarakis
  • Research Internship at Inria, 2014-04 to 2014-09:
    Formally Verified Tag-Based Enforcement of Control Flow Integrity (thesis)
  [MSc Student at NTU Athens] [Then MPRI MSc student] [Then PhD student at Princeton University]
  [Then PostDoc at University of Wisconsin-Madison] [Now Senior Applied Scientist at Amazon Web Services (AWS)]
• Alex Busenius
  • Master's Thesis, Finished 2011-04-04:
    Mechanized Formalization of a Transformation from an Extensible Spi Calculus to Java
  • Bachelor's Thesis, Finished 2008-10-28:
    Expi2Java - An Extensible Code Generator for Security Protocols
  [Student at Saarland University] [Now Technical Lead at Luxoft]
• Thorsten Tarrach
  • Master's Thesis, Finished 2010-08-31:
    Automatically Verifying "M" Modeling Language Constraints (thesis)
  • Bachelor's Thesis, Finished 2008-10-27:
    Spi2F# - A Prototype Code Generator for Security Protocols
  [Student at Saarland University] [Then PhD student at IST Austria] [Then research engineer at the Austrian Institute of Technology (AIT)] [Now Senior Applied Scientist at Amazon Web Services (AWS) in the S3 Automated Reasoning Group]
• Martin Grochulla
  • Master's Thesis, Finished 2009-01-06 (co-advised with Matteo Maffei)
    Security Despite System Compromise with Zero-Knowledge Proofs
  [Student at Saarland University] [Then PhD student at the MPI-INF] [Now IT Project Manager at Mercedes-Benz]