SMACK Verification Frontend

SMACK translates LLVM bitcode into Boogie programs for verifier backends. The SMACK implementation lives under third-party/verification/smack/ and the command-line frontend under tools/verifier/smack/.

docs/source/verification/smack/ holds the upstream SMACK documentation, kept in-tree so that it stays next to the frontend.

Upstream documentation

• Installation

• Running SMACK

• Usage notes

• Boogie code generation

• FAQ

• Demos

• Projects

• Publications

• People

• Code of conduct

Build Targets

• SmackUtils / SmackTranslator - migrated SMACK library targets

• llvm2bpl - LLVM-to-Boogie translator

• smack - frontend script installed with the verifier tools

See Also

• CLAM – Abstract Interpretation Framework - CLAM abstract interpretation frontend

• SeaHorn Verification Framework - SeaHorn verification frontend

• Verification Driver Abstraction - verification backend overview