Papers & Talks

Publications

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification, Son Ho, Aymeric Fromherz, Jonathan Protzenko, (ICFP 2023).

Aeneas: Rust Verification by Functional Translation, Son Ho, Jonathan Protzenko. (ICFP 2022). long version. talk.
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations, Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan. (S&P’22).

Proof-Producing Synthesis of CakeML from Monadic HOL Functions, Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan, Journal of Automated Reasoning (JAR), 2020, Springer.

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions, Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O.Myreen, Yong Kiam Tan, and Michael Norrish,
In Automated Reasoning - 9th International Joint Conference (IJCAR), Didier Galmiche and Stephan Schulz and Roberto Sebastiani (editors), 2018, Springer.
Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications,
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho,
In Verified Software. Theories, Tools, and Experiments (VSTTE), Ruzica Piskac and Philipp Rümmer (editors), 2018, Springer.

Aeneas: Rust Verification by Functional Translation, I gave variations of this talk at various institutions and workshops, including different Inria institutes, MSR, the NUS, or the Rust Formal Methods Interest Group. PDF

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.

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

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