Cătălin Hriţcu

Registered user since Wed 27 May 2015

Name: Cătălin Hriţcu

Bio: 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.

Country: Germany

Affiliation: MPI-SP

Personal website: http://prosecco.gforge.inria.fr/personal/hritcu/

Research interests: Formal methods for security

Contributions

CPP 2021Co-chair in Program Committee within the CPP 2021-track
Steering Committee Member in Steering Committee within the CPP 2021-track
PC and Conference Co-Chair in Organization Committee within the CPP 2021-track
PriSC 2020Author of Trace-Relating Compiler Correctness and Secure Compilation within the Principles of Secure Compilation 2020-track
Chair in Steering Committee within the Principles of Secure Compilation 2020-track
CPP 2020Author of PC Chairs' report within the CPP 2020-track
Session Chair of Invited talk (part of CPP 2020)
Program Co-Chair in Program Committee within the CPP 2020-track
POPL 2020Author of The Next 700 Relational Program Logics within the Research Papers-track
PriSC 2019Committee Member in Organizing Committee within the PriSC 2019-track
ESOP 2019Author of Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms within the ESOP 2019-track
POPL 2019Artifact Evaluation Co-Chair in Organizing Committee
Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the Artifact Evaluation-track
ML 2018Author of ML as a Tactic Language, Again within the ML 2018-track
ICFP 2019Author of Dijkstra Monads for All within the Research Papers-track
PriSC 2018Author of Short talk: The Meaning of Memory Safety within the PriSC 2018-track
Author of Robust Hyperproperty Preservation for Secure Compilation within the PriSC 2018-track
Session Chair of Welcome and Invited Talk (part of PriSC 2018)
Author of Formally Secure Compilation of Unsafe Low-Level Components within the PriSC 2018-track
Program Chair in Program Committee within the PriSC 2018-track
Program Chair of PriSC Welcome within the PriSC 2018-track
Organizer in Organizing Committee within the PriSC 2018-track
CPP 2018Author of A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations within the CPP 2018-track
HOPE 2017Author of Recalling a Witness within the HOPE 2017-track
SCM 2017Committee Member in Organizing Committee within the SCM-track
Presenter of What is Secure Compilation? Part II (Short talk) within the SCM-track
ICFP 2017Author of Verified Low-Level Programming Embedded in F* within the Research Papers-track
POPL 2018Author of Recalling a Witness: Foundations and Applications of Monotonic State within the Artifact Evaluation-track
Author of Recalling a Witness: Foundations and Applications of Monotonic State within the Research Papers-track
Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the Artifact Evaluation-track
Artifact Evaluation Co-Chair in Organizing Committee
TyDe 2016Committee Member in Program Committee within the TyDe-track
POPL 2017Committee Member in Program Committee within the POPL-track
Author of Beginner's Luck: A Language for Property-Based Generators within the POPL-track
Session Chair of Security and Privacy (part of POPL)
Author of Dijkstra Monads for Free within the POPL-track
PPS 2016Author of Making our Own Luck: A Language for Random Generators within the PPS 2016-track
CPP 2016Committee Member in Program Committee within the CPP-track
POPL 2016Author of Dependent Types and Multi-Monadic Effects in F* within the Research Papers-track
PLAS 2015Author of Micro-Policies: Formally Verified, Tag-Based Security Monitors within the PLAS-track