×

SMACK

swMATH ID: 23311
Software Authors: Carter, M., He, S., Whitaker, J., Rakamarić, Z., Emmi, M.
Description: 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.
Homepage: http://smackers.github.io/
Related Software: CBMC; z3; KLEE; CPAchecker; SeaHorn; VCC; Frama-C; UFO; LLVM; Crust; Viper; Joogie; Boogie; SMT-LIB; Cascade; SatAbs; BoogiePL; Predator; LLBMC; BVD
Cited in: 8 Publications

Standard Articles

1 Publication describing the Software Year
SMACK: Decoupling source language details from verifier implementations
Rakamarić, Zvonimir; Emmi, Michael
2014

Citations by Year