back to home page

Cătălin Hriţcu

Publications

bibtex file

Journal Papers

• Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy. Semantic Subtyping with an SMT Solver. To appear in Journal of Functional Programming, December 2011.
  • More information can be found on the Dminor project website at Microsoft Research.
  • An abridged version appeared in 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), September 2010
  • A Microsoft Research technical report (MSR-TR-2010-99) contains additional details and full proofs, December 2011.
  • The Dminor model and some of the proofs in this paper are formalized in Coq, November 2010.
• Cătălin Hriţcu, Jan Schwinghammer. A Step-indexed Semantics of Imperative Objects. Logical Methods in Computer Science (LMCS), 5(4), December 2009.
  • A preliminary version of this work was presented at the Workshop on Foundations of Object-Oriented Languages (FOOL'08), January 2008.

Conference Papers

• 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.
  • Implementation, Coq proofs and additional details available on the page of the DVerify project.
• Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Union and Intersection Types for Secure Protocol Implementations. To appear in Theory of Security and Applications (TOSCA'11), Invited paper, April 2011.
  • Full version that contains additional technical details, February 2011.
  • Prototype implementation (F5) by Thorsten Tarrach and Cătălin Hriţcu, November 2010.
  • Machine-checked soundness proof in Coq by Cătălin Hriţcu, February 2011.
  • A very preliminary version of this work was presented at FCS'09, August 2009.
• 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.
• 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.
  • Full version that contains all the technical details, March 2009.
  • Prototype of the protocol transformation by Martin Grochulla, March 2009.
  • A preliminary version of this paper was presented at ARSPA-WITS'09, March 2009.
• 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.
  • Machine-checked soundness proof in Coq by Cătălin Hriţcu, May 2011.
  • Full version that additionally contains all the technical details of the type system, a brief discussion about security despite compromise, and all the proofs, November 2008.
  • Implementation of the type-checker for zero-knowledge by Stefan Lorenz, Kim Pecina, Cătălin Hriţcu, and Thorsten Tarrach, September 2008.
  • A preliminary version of this paper was presented at FCS-ARSPA-WITS'08, June 2008.
• 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.
• Cătălin Hriţcu, Sabin Buraga. A Reference Implementation of ADF (Agent Developing Framework): Semantic Web-Based Agent Communication. Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), pages 199-206, IEEE Computer Society Press, September 2005.

Workshop Presentations

• Michael Backes, Cătălin Hriţcu, and Thorsten Tarrach. Automatically Verifying Typing Constraints for a Data Processing Language. First International Workshop On Intermediate Verification Languages (BOOGIE 2011), July 2011.
  • Implementation, Coq proofs and additional details available on the page of the DVerify project.
• Michael Backes, Cătălin Hriţcu, Matteo Maffei, and Thorsten Tarrach. Type-checking Implementations of Protocols Based on Zero-knowledge Proofs - Work in Progress. Workshop on Foundations of Computer Security (FCS'09), August 2009.
• Michael Backes, Martin Grochulla, Cătălin Hriţcu, and Matteo Maffei. Achieving Security Despite Compromise Using Zero-knowledge. Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09), March 2009.
• Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Type-checking Zero-knowledge. Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS'08), June 2008.
• Cătălin Hriţcu, Jan Schwinghammer. A Step-indexed Semantics of Imperative Objects. Workshop on Foundations of Object-Oriented Languages (FOOL'08), January 2008.
• Cătălin Hriţcu, Iulian Goriac, Raluca Gordân, Elena Erbiceanu. Designing a Multi-Precision Number Theory Library. NATO Advanced Research Workshop on Concurrent Information Processing and Computing, July 2003.
  • Implemented as the MpNT library.

Unpublished Technical Reports

• Ferucio Țiplea, Sorin Iftene, Cătălin Hriţcu, Iulian Goriac, Raluca Gordân, Elena Erbiceanu. MpNT: A Multi-precision Number Theory Library. Number Theoretical Algorithms (I), Technical Report TR03-02, Faculty of Computer Science, "Alexandru Ioan Cuza" University, Iaşi, May 2003.

Theses

• Cătălin Hriţcu. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD Thesis Draft. Advisors: Michael Backes, Matteo Maffei, and Andrew D. Gordon (MSR), Saarland University, Saarbrücken, Germany, Submitted November 2011.
  • Coq formalizations, implementations, samples, and further details available on the pages of the Zero-knowledge Type-checker and of the F5 Toolchain for RCF.
• Cătălin Hriţcu. Step-indexed Semantic Model of Types for the Functional Object Calculus. Master's Thesis, Advisor: Jan Schwinghammer, Saarland University, Saarbrücken, Germany, May 2007.
  • Awarded the Günter-Hotz Medal by the "Freunde der Saarbrücker Informatik".
• Cătălin Hriţcu. Agent Developing Platform: Agent Communication. Licentiate Thesis. Advisor: Sabin Buraga, "Alexandru Ioan Cuza" University of Iaşi, Romania, June 2005.
  • Implemented as the ADF platform.

Other

• Sergiu Dumitriu, Marta Gîrdea, Cătălin Hriţcu. Building Interactive Web Interfaces Using SVG Components. Romanian Human-Computer Interaction Conference (RoCHI 2005), September 2005.
• Sergiu Dumitriu, Marta Gîrdea, Cătălin Hriţcu. sMArTH: Mathematical Expressions on the Web. Romanian Human-Computer Interaction Conference (RoCHI 2005), September 2005.
  • Implemented as the sMArTH online equation editor.