| master |  |
develop |  |
|---|
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 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. 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 the
Boogie and Corral
verifiers.
See below for system requirements, installation, usage, and everything else.
We are very interested in your experience using SMACK. Please do contact
Zvonimir or
Michael with any possible feedback.
Support
-
For general questions, first consult the FAQ.
-
If something is otherwise broken or missing, open an issue.
-
To stay informed about updates, you can either watch SMACK's Github page,
or you can join SMACK's Google Group
mailing list. Even without a Google account, you may join by sending mail to
smack-dev+subscribe@googlegroups.com.
Acknowledgements
SMACK project is partially supported by NSF award CCF 1346756 and Microsoft
Research SEIF award. We also rely on University of Utah's
Emulab infrastructure for extensive benchmarking of
SMACK.