Cătălin Hriţcu
From July 2007 until January 2012 I was a PhD student
in Computer
Science at Saarland
University in
the Information
Security and Cryptography Group. My current webpage is still
hosted here.
News
Starting in May 2011 I am Research Associate at the University of Pennsylvania, working on the CRASH/SAFE project under the guidance of Prof. Benjamin C. Pierce.
Office: Moore GRW 078
Office Phone: +1-215-898-5886
- Address:
-
University of Pennsylvania, CIS dept.
3330 Walnut Street
Philadelphia, PA 19104-6389
Research Interests
- Language-based Security
- Type systems
- Semantics of Programming Languages
- Verification
- Formal Methods in Software Engineering
Recent Publications and Drafts
Here is my complete list of publications (also on Google Scholar, MS Academic Search, and DBLP).
- 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.
- Online appendix containing details that had to be omitted in the NFM paper due to the lack of space.
- Implementation, case studies, documentation, Coq formalization, and proofs are all available on the page of the expi2java project.
- Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations, Submitted to special issue of the Journal of Computer Security (JCS) for TOSCA-SecCo, January 16, 2012.
- Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy. Semantic Subtyping with an SMT Solver. Journal of Functional Programming, Cambridge University Press, March 2012.
- 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), December 2011.
Recent Talks
Here is my complete list of talks.
- Software Foundations
- On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
- Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis
- Thesis defense, Saarland University: slides (2012-01-10)
- Featherweight Breeze
- Breeze: A Language For Writing Secure Software
- Union, Intersection, and Refinement Types and Reasoning about Type Disjointness for Analyzing Protocol Implementations
- Control Hijacking: Defenses
- Semantic Subtyping with an SMT Solver
Students
- Alex Busenius
- Thorsten Tarrach
- Martin Grochulla
Teaching Assistant
Contact
E-mail (preferred): catalin.hritcu@gmail.com
(More ways to find me)
Misc
