Publications

2022

2021

2020

2018

Talks

2023

  • Aeneas: Rust Verification by Functional Translation, I gave variations of this talk at Inria Grenoble, Inria Rennes, ProLang@Inria and the Rust Formal Methods Interest Group. PDF

2022

  • Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations, S&P’22. teaser. PPTX

  • Aeneas: Rust Verification by Functional Translation, Cambium seminar at Inria Paris. PDF.

2021

  • Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations, I gave variations of this talk at Inria Paris and at MSR. PDF.

2018

  • Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions, IJCAR 2018. PDF.