Vincent Laporte

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).

Publications

See dblp for a complete list.

Research projects

Jasmin

Jasmin is a programming language to write high-assurance, high-speed cryptographic implementations.

Its compiler is correct — formally verified in Coq.

Verasco

Verasco is a formally-verified static analyzer for C.