Leveraging Rust Types for Modular Specification and Verification

Citation: Vytautas Astrauskas, Peter Müller, Federico Poli, Alexander J. Summers Leveraging Rust Types for Modular Specification and Verification.
Internet Archive Scholar (search for fulltext): Leveraging Rust Types for Modular Specification and Verification
Wikidata (metadata): Q60432227
Tagged:

Summary

Describes verification for subset of Rust utilizing Rust types and the Rust compiler, with programmer-provided annotations. Programmers do not interact with underlying proof mechanism, allowing programs to be verified without the involvement of verification experts.