A Bounded Software Verifier for C Programs GitHub


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. 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. By default, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well.


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



Leave Us a Message

Contact Us

SOAR LabPO Box 345678 Salt Lake City, UtahUnited States