About Me  |  CV  |  Research Interests  |  Publications  |  Teaching  

I have moved to FireEye Germany . This webpage will still be updated.

About me

Currently, I am working as a Verification Engineer in FireEye formal methods team in Dresden, Germany.
I used to be a PhD. student at IMDEA Software under the supervision of Gilles Barthe.
I received my degree (Licenciado) in Computer Science on April of 2009 from Universidad Nacional de Rosario, Argentina. It is a five year degree with thesis, roughly equivalent to a Master degree in the EU system.

Curriculum Vitæ

Here you can download the most updated version of my cv.

Research Interests

My main research interests are:

• Program Verifcation
• Verification of Cryptographic Systems
• Programming Language Semantics
• Security

Peer-Reviewed Papers (at DBLP)

• Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt: Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols. EUROCRYPT (2) 2015: 689-718.


• Gilles Barthe, Juan Manuel Crespo, Benjamin Gregoire, Cesar Kunz, Yassine Lakhnech, Benedikt Schmidt and Santiago Zanella-Beguelin: Fully Automated Analysis of Padding-Based Encryption in the Computational Model. ACM CCS 2013. [PDF|BIB]


• Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz and Mark Marron: From Relational Verification to SIMD Loop Synthesis. ACM PPoPP 2013. [PDF|BIB]


• Gilles Barthe, Juan Manuel Crespo and César Kunz. Beyond 2-safety: asymmetric product programs for relational program verification. LFCS 2013: 29-43.[PDF|BIB]


• Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas: Secure Multi-Execution through Static Program Transformation. FMOODS/FORTE 2012: 186-202.[PDF|BIB]


• Juan Manuel Crespo, Cesar Kunz: A machine-checked framework for relational separation logic. SEFM 2011: 122-137.[PDF|BIB]


• Gilles Barthe, Juan Manuel Crespo, Cesar Kunz: Relational Verification Using Product Programs. FM 2011: 200-214.[PDF|BIB]


• Juan Manuel Crespo, Gustavo Betarte, Carlos Luna: A Framework for the Analysis of Access Control Models for Interactive Mobile Devices. TYPES 2008: 49-63.[PDF|BIB]

Invited Papers

• Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin: Computer-Aided Cryptographic Proofs. ITP 2012: 11-27 [PDF| BIB]

Technical Reports

• Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt: Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. IACR Cryptology ePrint Archive 2015: 074, February 2015. [PDF| BIB]


• Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin: Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptology ePrint Archive 2012: 695, December 2012. [PDF| BIB]


• Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas, Secure multi-execution through static program transformation: extended version, Technical Report (CW Reports), volume CW620, Department of Computer Science, KU Leuven, April 2012. [PDF| BIB]

Awards

• FPI Scholarship (BES-2010-031271). Science and Innovation Ministry, Spain.
• PPOPP 2013 Best paper Award for "From Relational Verification to SIMD Loop Synthesis"
• CACM Nomination for "From Relational Verification to SIMD Loop Synthesis"

Teaching

At Rosario I used to be Teaching Assistant. From July of 2006 to April 2009 I was involved in the following courses:

• Data Structures
• Programming Language Analisys II (Functional Programming).
• Formal Construction of Programs (Type Theory).
• Discrete Mathematics