Experiments in using the Smack verification tool with C and Rust.

These are mostly just explorations of the tool but I am making them available in case they are useful to others.

SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. Under the hood, SMACK is a translator from the LLVM compiler's popular intermediate representation (IR) into the Boogie intermediate verification language (IVL). Sourcing LLVM IR exploits an increasing number of compiler front-ends, optimizations, and analyses. Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. – SMACK homepage

So, it supports many different languages, it is fairly low effort to start using, but, because it is a bounded verifier, it proves that a program does not have bugs up to some bound/depth but it makes no guarantees beyond that bound.

1. Installing SMACK
2. Using SMACK – quick sketch/demo
3. SMACK examples – detailed examples
4. SMACK issues - problems I ran into