Hi KLEE-devs, A quick update on where we got to with Rust verification over at Google
- We am able to compile/link most Rust programs to generate LLVM bitcode. (The main obstacle at the moment is crates that include C code.) - We can run KLEE on that bitcode directly Details: https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-klee.md - Compiling and then running KLEE is quite complicated because you need lots of obscure Rust flags to make it work. So, we have written a script 'cargo-verify' that hides a lot of the complexity Details: https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-annotations.md - A major theme in our research project is trying to narrow the gap between dynamic verification (aka testing) and static verification (aka formal verification). So we have reimplemented the 'proptest' property-testing library so that it can be used with a formal verification tool. This lets you write a single test harness and then choose to use it either with the proptest library (dynamic verification) or with our 'propverify' library and KLEE (static verification). Details: https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-propverify.md The complete collection of tools and libraries are open-sourced using the usual Rust licenses. https://github.com/project-oak/rust-verification-tools This is very much a research prototype at this stage - more interesting than useful. -- Alastair
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
