← All papers
Simple Verification of Rust Programs via Functional Purification
cs.LO
Jan 1, 2020 · v1
TL;DR
Translates Rust programs into Lean's functional representation for verification via ownership analysis.
Abstract
This master's thesis presents an approach to verifying Rust programs by translating them into a purely functional representation in the Lean theorem prover. The translation exploits Rust's ownership type system to extract a functional semantics, enabling verification of imperative Rust code using Lean's proof capabilities.
Problem
Verifying imperative Rust programs for correctness is difficult because verification tools must reason about mutable state, aliasing, and control flow. Existing approaches often require heavyweight annotations or specialized logics.
Approach
The thesis translates Rust programs into a purely functional representation in the Lean theorem prover. It exploits Rust's ownership type system to extract a functional semantics from imperative code, enabling verification using Lean's standard proof capabilities without specialized separation logic.
Results
The approach demonstrates that Rust's ownership discipline provides enough structure to derive functional equivalents amenable to Lean verification, enabling proof of correctness for imperative Rust programs.