46 citations · 47 across the 3 of their papers we have counts for
4 papers
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Son Ho, Cédric Fournet, Jonathan Protzenko +7
We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…
Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
Son Ho, Aymeric Fromherz, Jonathan Protzenko
The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foun…
Aeneas: Rust Verification by Functional Translation
Son Ho, Jonathan Protzenko
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memor…
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
Son Ho, Aymeric Fromherz, Jonathan Protzenko
For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-sca…