RustProof: Static Analysis Using MIR - PDXRust October 2016

Explore a conference talk from PDXRust October 2016 where a PSU Capstone team presents their progress on static analysis using MIR for RustProof. Delve into the benefits of formal verification, Hoare Logic, and verification condition generation. Learn about compiler plugins, parsing techniques, and solving methods employed in the project. Discover the supported Rust language features and understand the concept of weakest preconditions. Gain insights into the challenges faced during development and participate in a Q&A session to further your understanding of this innovative approach to Rust programming.

Intro
Preface
Benefits of Formal Verification
Hoare Logic Primer
Verification Condition Generation
Compiler Plugins
Parsing, VC Generation, Solving
Problems we encountered
Supported Rust Language Features
Questions?
Weakest Preconditions