Post-doctoral Researcher at Imdea Software Institute, working with prof. Gilles Barthe.
Currently on leave at Inria Sophia Antipolis, in the Marelle team (since October 2017).
E-mail: vlaporte [at] imdea.org
PGP: EBD582AD DDB1F81F
Phone: 0 (033) 4 92 38 77 95
Curriculum vitæ (pdf, 68 Kio).
See dblp for a complete list.
Jasmin is a programming language to write high-assurance, high-speed cryptographic implementations.
Its compiler is correct — formally verified in Coq.
Verasco is a formally-verified static analyzer for C.