Papers & Talks

Publications

Formal Verification of Rust Programs by Functional Translation, Son Ho, (PhD Thesis). [ bib | ppt ].
Charon: An Analysis Framework for Rust, Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko, (preprint). [ bib ].
Sound Borrow-Checking for Rust via Symbolic Semantics, Son Ho, Aymeric Fromherz, Jonathan Protzenko, (ICFP 2024). [ bib | long version ].
Incremental Proof Development in Dafny with Module-Based Induction, Son Ho, Clément Pit-Claudel, (Dafny Workshop). [ bib ].

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

Aeneas: Rust Verification by Functional Translation, Son Ho, Jonathan Protzenko. (ICFP 2022). [ bib | 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). [ bib | long version | talk ]

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. [ bib ]

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). [ bib ]
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). [ bib ]