Verification of safety functions implemented in Rust: A symbolic execution based approach

Marcus Lindner, Nils Fitinghoff, Johan Eriksson, Per Lindgren
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 12 May 2020

Proceedings : 2019 IEEE 17th International Conference on Industrial Informatics (INDIN)
IEEE International Conference on Industrial Informatics (INDIN)
Luleå University of Technology, Computer Science
Pages 432-439
2019
Note(s): Rust language, symbolic execution, extended static checking, KLEE verifier
Papers: lindner:indin:2018

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.