SMACK Verification Frontend

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

The upstream SMACK documentation has been copied into this repository under docs/source/verification/smack/ so it can be updated alongside the migrated frontend.

Copied 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