Explore a prototype tool for verifying Rust software in this 24-minute conference talk by Xavier Denis. Dive into the world of Creusot, learning about its approach to translating Rust code, the program logic it employs, and the concept of prophetic values. Examine practical examples, understand the current state of specifications, and gain insights into logic functions. Discover the ongoing and future work in this field, including the intriguing "All Zero" concept, as you delve deeper into the realm of Rust software verification.
Creusot: A Prototype Tool for Verification of Rust Software
Overview
Syllabus
Intro
Verifying Rust
Verification in Creusot
Translating Rust
A program logic for Rust
Prophetic Values
Example
State of specifications
Notes on Logic Functions
All Zero
Ongoing / Future Work
Taught by
Rust
