About Me
I am a post-doctoral researcher at IMDEA, under the supervision of Gilles Barthe, and working on proving concrete realizations and implementations of cryptographic primitives and protocols secure.
My Ph.D. dissertation on "Proving C Programs Secure with general-Purpose Verification Tools" was accepted at the Open University in April 2013, after minor corrections. It was written under the supervision of Andy Gordon, Jan Jürjens and Bashar Nuseibeh.
Research Interests
My current research interests are mainly in the formal verification of imperative programs, with a focus on computational cryptographic security properties.
In the past, I have worked on abstract interpretation and some aspects of programming and natural languages.
Selected Publications
-
A more complete list of my publications is available here.
-
Proving Cryptographic C Programs Secure with General-Purpose Verification Tools, Ph.D. Thesis.
-
Proving Computational Security with a General-Purpose C Verifier, with Cédric Fournet and Andrew D. Gordon.
In submission. -
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, with Andrew D. Gordon, Jan Jürjens and David A. Naumann. CSF'11, Paris, June 2011, pages 3--17.