Bruno Blanchet

My research area is static program analysis, by abstract interpretation, to verify or optimize programs. I have worked in particular on the verification of cryptographic protocols and on the optimization of memory management in the languages ML and Java. For more information, have a look at the following pages:

Publications

Talks

Teaching at MPRI (Parisian Master of Research in Computer Science), course 2-30 Cryptographic protocols: formal and computational proofs

Conferences:

• CCS'10 (PC member)
• CSF'10 (PC member)
• TACAS'10 (PC member)
• ASIAN'09 (PC member)
• ECRYPT-II summer school (Invited speaker)

Associate Editor International Journal of Applied Cryptography (IJACT)

Coordinator of the Formacrypt project.

Research interests:

• Analysis of cryptographic protocols in the formal model, verifier ProVerif
• Analysis of cryptographic protocols in the computational model, verifier CryptoVerif
• Verification of critical software, Official Astrée project page
• Escape analysis, stack allocation and synchronization elimination (DEA training and PhD thesis)

Here are a few pointers towards my older work.

• "Magistère" report
• The GOI machine (master's training)
• Caml-Light with dimensions (master's project)

Links