back to home page

Cătălin Hriţcu

Publications

bibtex file

Conference Papers

  1. Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. Recalling a Witness: Foundations and Applications of Monotonic State. Conditionally Accepted at POPL'18, July 2017.
  2. Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy, Verified Low-Level Programming Embedded in F*. In 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2017. To appear.
  3. Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Cătălin Hriţcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS. 2nd Summit on Advances in Programming Languages (SNAPL), May 2017.
  4. Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 515--529. ACM, January 2017.
  5. Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Li-yao Xia. Beginner's Luck: A Language for Random Generators. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 114--129. ACM, January 2017.
  6. Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In 29th IEEE Symposium on Computer Security Foundations (CSF). To appear. arXiv:1602.04503. Author Preprint of May 6 2016.
  7. Nikhil Swamy, Cătălin Hriţcu, 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*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256-270, January 2016.
  8. Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 325-343. Springer, August 2015.
  9. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 36th IEEE Symposium on Security and Privacy (Oakland S&P), pages 813-830. IEEE Computer Society, May 2015.
  10. Udit Dhawan, Cătălin Hriţcu, Nikos Vasilakis, Raphael Rubin, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce, and André DeHon. Architectural Support for Software-Defined Metadata Processing. In 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 487-502. ACM, March 2015.
  11. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 165-178. ACM, January 2014.
  12. Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos. Testing Noninterference, Quickly. In 18th ACM SIGPLAN International Conference on Functional Programming (ICFP). pages 455-468, ACM Press. September 2013.
  13. Cătălin Hriţcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett. All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy (Oakland), pages 3-17, IEEE Computer Society Press, May 2013.
  14. Michael Backes, Alex Busenius, Cătălin Hriţcu. On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. 4th NASA Formal Methods Symposium (NFM 2012), pages 371-387, April 2012.
  15. Michael Backes, Cătălin Hriţcu, and Thorsten Tarrach. Automatically Verifying Typing Constraints for a Data Processing Language. In First International Conference on Certified Programs and Proofs (CPP 2011), pages 296-313, Springer, December 2011.
  16. Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Union and Intersection Types for Secure Protocol Implementations. In Theory of Security and Applications (TOSCA'11), Invited paper, April 2011.
  17. Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy. Semantic Subtyping with an SMT Solver, In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), September 2010.
  18. Michael Backes, Martin Grochulla, Cătălin Hriţcu, and Matteo Maffei. Achieving Security Despite Compromise Using Zero-knowledge. In 22th IEEE Symposium on Computer Security Foundations (CSF 2009), pages 308-323, IEEE Computer Society Press, July 2009.
  19. Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Type-checking Zero-knowledge. In 15th ACM Conference on Computer and Communications Security (CCS 2008), pages 357-370, ACM Press, October 2008.
  20. Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus. In 21th IEEE Symposium on Computer Security Foundations (CSF 2008), pages 195-209, IEEE Computer Society Press, June 2008.

Journal Papers

  1. Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, and Dimitrios Vytiniotis. Testing Noninterference, Quickly. Special Issue of Journal of Functional Programming (JFP) for ICFP 2013. 26:e4 (62 pages), April 2016.
  2. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. Journal of Computer Security (JCS); Special Issue on Verified Information Flow Security, 24(6):689--734, December 2016.
  3. Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations, Journal of Computer Security (JCS); Special Issue on Foundational Aspects of Security, 22(2):301-353, February, 2014.
  4. Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy. Semantic Subtyping with an SMT Solver. Journal of Functional Programming, 22(1):31-105, Cambridge University Press, March 2012.
  5. Cătălin Hriţcu, Jan Schwinghammer. A Step-indexed Semantics of Imperative Objects. Logical Methods in Computer Science (LMCS), 5(4), December 2009.

Book

  1. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations, Electronic textbook, 2017.

PhD Thesis

  1. Cătălin Hriţcu. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD Thesis, Saarland University, January 2012.

Informal

  1. Arthur Azevedo de Amorim, Cătălin Hriţcu, and Benjamin C. Pierce.
    The Meaning of Memory Safety. arXiv:1705.07354, August 2017.
  2. Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations. arXiv:1703.00055, July 2017.
  3. Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. Technical Report, arXiv:1510.00697, October 2015.
  4. Alejandro Aguirre, Cătălin Hriţcu, Chantal Keller, and Nikhil Swamy. From F* to SMT (extended abstract). Talk at 1st International Workshop on Hammers for Type Theories (HaTT), July 2016.
  5. Udit Dhawan, Albert Kwon, Edin Kadric, Cătălin Hriţcu, Benjamin C. Pierce, Jonathan M. Smith, Gregory Malecha, Greg Morrisett, Thomas F. Knight, Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan, and André DeHon, Hardware Support for Safety Interlocks and Introspection. In SASO Workshop on Adaptive Host and Network Security, September 2012.