This paper describes the
cargo-Rust that allows the KLEE verifier
to be used to verify Rust programs.
KLEE is a symbolic execution tool so using it to verify code leads
to a path explosion problem.
The solution taken in this paper is to use a contract driven development
approach to enable modular verification.
This reduces the path explosion problem to only involve the number of
paths per function instead of the number of paths through the entire
Papers related to No panic! Verification of Rust programs by symbolic execution
- Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]