This paper looks at how to use the KLEE verifier to verify code implementing a state machine written in Rust based on their earlier work (lindner:indin:2018). The challenge here is that KLEE is a symbolic execution tool and does not guarantee to explore all paths through the code to a sufficient depth to guarantee soundness. Their solution lies in constructing an appropriate verification harness.
Papers related to Verification of safety functions implemented in Rust: A symbolic execution based approach
- No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]