I am a PhD student at IMDEA Software Institute under the supervision of Gilles Barthe. I received a degree in computer science from the Universidad Nacional de Rosario (UNR), Argentina in December of 2008. It is a five years degree with thesis, roughly equivalent to a master degree in the EU system.

Research Interests

My main research topic is the application of formal methods to verify security properties of computer systems. The areas I am interested in are:

  • Cryptography and language-based security
  • Theorem provers
  • Programming language semantics
  • Program verification


Conference Articles

  • Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs.
    In 40th International Colloquium on Automata, Languages and Programming - ICALP 2013.
    [ BibTeX | PDF | Slides ]
  • Verifiable Indifferentiable Hashing into Elliptic Curves.
    In 1st Conference on Principles of Security and Trust - POST 2012.
    [ BibTeX | PDF | Slides ]
  • Probabilistic Relational Reasoning for Differential Privacy.
    In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2012.
    [ BibTeX | PDF | Slides ]
  • Verifiable Security of Boneh-Franklin Identity-Based Encryption.
    In 5th International Conference on Provable Security - ProvSec 2011.
    [ BibTeX | PDF | Slides ]
  • Formally certifying the security of digital signature schemes.
    In Proceedings of the 30th IEEE Symposium on Security and Privacy, S&P 2009.
    [ BibTeX | PDF | Slides ]

Journal Articles

  • Verifiable Indifferentiable Hashing into Elliptic Curves.
    To appear in Journal of Computer Security, IO Press, 2014.
    [ BibTeX | PDF ]
  • Probabilistic Relational Reasoning for Differential Privacy.
    In ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 35, Issue 3, ACM, 2013.
    [ BibTeX | PDF ]
You can find an up-to-date list of my publications in my DBLP entry.

PhD Thesis

Approximate Relational Reasoning for Probabilistic Programs.
To be examined in January 2014, Technical University of Madrid.
[ PDF ]


I contribute in the development of the CertiCrypt and CertiPriv tools. CertiCrypt is a framework built on top of the Coq proof assistant that enables the machine-checked construction and verification of language-based cryptographic proofs. CertiPriv is a tool built on top of CertiCrypt aimed at verifying differential privacy properties of probabilistic programs.


I worked at the Computer Science Department at UNR as a teaching assistant from August 2004 to December 2008 on different courses:

  • Introduction to Informatics
  • Analysis of Programming Languages I
  • Logic and Algorithms
  • Mathematical Analysis IV