Creusot: A Prototype Tool for Verification of Rust Software

Creusot: A Prototype Tool for Verification of Rust Software

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.