SMACK

Software Verifier and Verification Toolchain GitHub

About

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.

Publications

Our Team

Our Clients
Zvonimir Rakamaric
Our Clients
Michael Emmi
Our Clients
Montgomery Carter
Our Clients
Shaobo He
Our Clients
Pantazis Deligiannis
Our Clients
Arvind Haran
Our Clients
Jonathan Whitaker

FOLLOW US

Contact

Leave Us a Message

Contact Us

SOAR LabPO Box 345678 Salt Lake City, UtahUnited States