Vincent Laporte

Post-doctoral Researcher at Imdea Software Institute, working with prof. Gilles Barthe.

E-mail: Vincent [dot] Laporte [at] mailbox [dot] 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.