Cătălin Hriţcu

Registered user since Wed 27 May 2015

Name: Cătălin Hriţcu

Bio: Catalin Hritcu is a researcher at Inria Paris where he works on security foundations. He is particularly interested in formal methods for security (secure compilation, compartmentalization, memory safety, security protocols, integrity, information flow), programming languages (program verification, type systems, proof assistants, semantics, formal metatheory, certified tools, property-based testing), and the design and verification of security-critical systems (reference monitors, secure compilation chains, secure hardware). He was awarded an ERC Starting Grant on formally secure compilation and is also actively involved in the design of the F* verification system and its use for building a formally verified HTTPS stack. Catalin received his PhD from Saarland University. Recently he received a Habilitation degree from ENS Paris, and was also a Research Associate at University of Pennsylvania and a Visiting Researcher at Microsoft Research Redmond.

Country: France

Affiliation: Inria Paris

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

Research interests: Formal methods for security

Contributions

PriSC 2020Committee Member in Steering Committee within the Principles of Secure Compilation 2020-track
CPP 2020Program Co-Chair in Program Committee within the CPP 2020-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