Catalin Hritcu

ORCID

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 47

Top Venues

CoRR

Proc. ACM Program. Lang.

CSF

POPL

Saarland University (PHD)

Education History

Saarland University

PHD

Publications

Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Catalin Hritcu, Andrew Tolmach
SECOMP: Formally Secure Compilation of Compartmentalized C Programs. CoRR (2024)
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. CPP (2024)
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter
Securing Verified IO Programs Against Unverified Code in F. Proc. ACM Program. Lang. 8 (POPL) (2024)
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. ACM Trans. Program. Lang. Syst. 45 (3) (2023)
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. IACR Cryptol. ePrint Arch. 2023 (2023)
Cezar-Constantin Andrici, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
Securely Compiling Verified F* Programs With IO. CoRR (2023)
Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Deepak Garg, Catalin Hritcu
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation. CSF (2022)
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
An Extended Account of Trace-relating Compiler Correctness and Secure Compilation. ACM Trans. Program. Lang. Syst. 43 (4) (2021)
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. IACR Cryptol. ePrint Arch. 2021 (2021)
David Chisnall, Deepak Garg, Catalin Hritcu, Mathias Payer
Secure Compilation (Dagstuhl Seminar 21481). Dagstuhl Reports 11 (10) (2021)
Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Deepak Garg, Catalin Hritcu
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation. CoRR (2021)
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. CSF (2021)
Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu
Dynamic IFC Theorems for Free! CSF (2021)
Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu
Dynamic IFC Theorems for Free! CoRR (2020)
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
Trace-Relating Compiler Correctness and Secure Compilation. ESOP (2020)
Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder
The next 700 relational program logics. Proc. ACM Program. Lang. 4 (POPL) (2020)
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
Trace-Relating Compiler Correctness and Secure Compilation. CoRR (2019)
Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder
The Next 700 Relational Program Logics. CoRR (2019)
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
Dijkstra monads for all. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
Dijkstra Monads for All. CoRR (2019)
Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, Jérémy Thibault
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. CSF (2019)
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms. ESOP (2019)
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. CPP (2018)
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Andrew Tolmach
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. CCS (2018)
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. CoRR (2018)
Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Arthur Azevedo de Amorim, Ana Nora Evans, Carmine Abate, Roberto Blanco, Théo Laurent, Benjamin C. Pierce, Andrew Tolmach
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. CoRR (2018)
Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, Jérémy Thibault
Exploring Robust Property Preservation for Secure Compilation. CoRR (2018)
Amal Ahmed, Deepak Garg, Catalin Hritcu, Frank Piessens
Secure Compilation (Dagstuhl Seminar 18201). Dagstuhl Reports 8 (5) (2018)
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Recalling a witness: foundations and applications of monotonic state. Proc. ACM Program. Lang. 2 (POPL) (2018)
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
The Meaning of Memory Safety. POST (2018)
Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia
Beginner's luck: a language for property-based generators. POPL (2017)
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
. CoRR (2017)
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin
A Monadic Framework for Relational Verification (Functional Pearl). CoRR (2017)
Deepak Garg, Catalin Hritcu, Marco Patrignani, Marco Stronati, David Swasey
Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). CoRR (2017)
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue
Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL (2017)
Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Ana Nora Evans, Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach
Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract). CoRR (2017)
Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce
The Meaning of Memory Safety. CoRR (2017)
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
Recalling a Witness: Foundations and Applications of Monotonic State. CoRR (2017)
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
Dijkstra monads for free. POPL (2017)
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A verified information-flow architecture. J. Comput. Secur. 24 (6) (2016)
Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
Testing noninterference, quickly. J. Funct. Program. 26 (2016)
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce
Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization. CoRR (2016)
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin
Dependent types and multi-monadic effects in F. POPL (2016)
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, Benjamin C. Pierce
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. CSF (2016)
Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
Dijkstra Monads for Free. CoRR (2016)
Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia
Beginner's Luck: A Language for Property-Based Generators. CoRR (2016)
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
Micro-Policies: Formally Verified, Tag-Based Security Monitors. IEEE Symposium on Security and Privacy (2015)
Catalin Hritcu
The Joint EasyCrypt-F*-CryptoVerif School 2014. ACM SIGLOG News 2 (1) (2015)
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A Verified Information-Flow Architecture. CoRR (2015)
Udit Dhawan, Catalin Hritcu, Raphael Rubin, Nikos Vasilakis, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight Jr., Benjamin C. Pierce, André DeHon
Architectural Support for Software-Defined Metadata Processing. ASPLOS (2015)
Catalin Hritcu
Micro-Policies: Formally Verified, Tag-Based Security Monitors. PLAS@ECOOP (2015)
Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce
Foundational Property-Based Testing. ITP (2015)
Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. CoRR (2015)
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A verified information-flow architecture. POPL (2014)
Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
Testing Noninterference, Quickly. CoRR (2014)
Michael Backes, Catalin Hritcu, Matteo Maffei
Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations. J. Comput. Secur. 22 (2) (2014)
Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos
Testing noninterference, quickly. ICFP (2013)
Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett
All Your IFCException Are Belong to Us. IEEE Symposium on Security and Privacy (2013)
Udit Dhawan, Albert Kwon, Edin Kadric, Catalin Hritcu, Benjamin C. Pierce, Jonathan M. Smith, André DeHon, Gregory Malecha, Greg Morrisett, Thomas F. Knight Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David K. Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan
Hardware Support for Safety Interlocks and Introspection. SASO Workshops (2012)
Michael Backes, Alex Busenius, Catalin Hritcu
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. NASA Formal Methods (2012)
Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy
Semantic subtyping with an SMT solver. J. Funct. Program. 22 (1) (2012)
Michael Backes, Catalin Hritcu, Matteo Maffei
Union and Intersection Types for Secure Protocol Implementations. TOSCA (2011)
Michael Backes, Catalin Hritcu, Thorsten Tarrach
Automatically Verifying Typing Constraints for a Data Processing Language. CPP (2011)
Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy
Semantic subtyping with an SMT solver. ICFP (2010)
Catalin Hritcu, Jan Schwinghammer
A Step-indexed Semantics of Imperative Objects Log. Methods Comput. Sci. 5 (4) (2009)
Michael Backes, Martin P. Grochulla, Catalin Hritcu, Matteo Maffei
Achieving Security Despite Compromise Using Zero-knowledge. CSF (2009)
Michael Backes, Catalin Hritcu, Matteo Maffei
Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus. CSF (2008)
Michael Backes, Catalin Hritcu, Matteo Maffei
Type-checking zero-knowledge. CCS (2008)
Catalin Hritcu, Sabin C. Buraga
A Reference Implementation of ADF (Agent Developing Framework): Semantic Web-Based Agent Communication. SYNASC (2005)
Catalin Hritcu, Iulian Goriac, Raluca Mihaela Gordan, Elena Erbiceanu
Designing a Multi-Precision number Theory Library. Int. J. Comput. 2 (3) (2003)

Catalin Hritcu.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Catalin Hritcu