46 citations · 47 across the 3 of their papers we have counts for
Showing cs.PLShow all
3 papers · 1 filter
cs.PL2024★ 1 cited
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…
cs.PL2022★ 46 cited
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…
cs.PL2021
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…