SMACK Software Verifier & 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

People

Coordinators

Michael Emmi
Michael Emmi
Zvonimir Rakamaric
Zvonimir Rakamaric

Contributors

Montgomery Carter
Montgomery Carter
Pantazis Deligiannis
Pantazis Deligiannis
Arvind Haran
Arvind Haran
Shaobo He
Shaobo He
Jonathan Whitaker
Jonathan Whitaker