GitHub - smackers/smack: SMACK Software Verifier and Verification Toolchain (original) (raw)
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. SMACK handles complicated feature of the C language, including dynamic memory allocation, pointer arithmetic, and bitwise operations.
Under the hood, SMACK is a translator from the LLVMcompiler's popular intermediate representation (IR) into theBoogie intermediate verification language (IVL). Sourcing LLVM IR exploits an increasing number of compiler front-ends, optimizations, and analyses. Currently SMACK only supports the C language via the Clang compiler, though we are working on providing support for additional languages. Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation. Currently, SMACK leverages theBoogie and Corralverifiers.
See below for system requirements, installation, usage, and everything else.
We are very interested in your experience using SMACK. Please do contactZvonimir orMichael with any possible feedback.
Support
- For general questions, first consult the FAQ.
- If something is otherwise broken or missing, open an issue.
- As a last resort, send mail toMichael, Zvonimir, or both.
- To stay informed about updates, you can watch SMACK's Github page.
Acknowledgements
SMACK project has been partially supported by funding from the National Science Foundation, VMware, Amazon, and Microsoft Research. We also rely on University of Utah's Emulab infrastructure for extensive benchmarking of SMACK.