Repository files navigation

SMACK is both amodular software verification toolchain and aself-contained software verifier. It can be used to verify the assertionsin its input programs. In its default mode, assertions are verified up to agiven bound on loop iterations and recursion depth; it contains experimentalsupport for unbounded verification as well. SMACK handles complicated featureof the C language, including dynamic memory allocation, pointer arithmetic, andbitwise operations.

Under the hood, SMACK is a translator from theLLVMcompiler'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 viatheClang compiler, though we are working on providingsupport for additional languages. Targeting Boogie exploits a canonicalplatform which simplifies the implementation of algorithms for verification,model checking, and abstract interpretation. Currently, SMACK leverages theBoogie andCorralverifiers.

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.

• For general questions, first consult theFAQ.

• If something is otherwise broken or missing, open anissue.

• As a last resort, send mail toMichael,Zvonimir, or both.

• To stay informed about updates, you can watch SMACK's Github page.

SMACK project has been partially supported by funding from the National ScienceFoundation, VMware, Amazon, and Microsoft Research. We also rely on University ofUtah'sEmulab infrastructure for extensivebenchmarking of SMACK.

1. System Requirements and Installation
2. Running SMACK
3. Demos
4. FAQ
5. Inline Boogie Code
6. Contribution Guidelines
7. Projects
8. Publications
9. People