Verifier Tools

This page documents verification tools under tools/verifier/. These tools focus on program verification, abstract interpretation, and model checking.

CLAM – Numerical Abstract Interpretation

CLAM is a static analysis framework based on abstract interpretation over numerical abstract domains. It is designed for inferring invariants and checking safety properties over LLVM bitcode.

Binaries: clam, clam-pp, clam-diff Location: tools/verifier/clam/

Quick Start:

# Analyze with interval domain
./build/bin/clam --crab-dom=int --crab-check program.bc

# Preprocess bitcode
./build/bin/clam-pp program.bc -o prep.bc

# Compare analysis results
./build/bin/clam-diff baseline.json modified.json

For detailed documentation, see CLAM – Numerical Abstract Interpretation.

SymAbsAI – Symbolic Abstraction + Abstract Interpretation

SymAbsAI is a framework for static program analysis using symbolic abstraction to provide a flexible interface for designing program analyses in a compositional way.

Binary: lotus-verify-symabs-ai Source: tools/verifier/symabs-ai/lotus-verify-symabs-ai.cpp

Quick Start:

# Analyze all functions
./build/bin/lotus-verify-symabs-ai example.bc

# Analyze specific function
./build/bin/lotus-verify-symabs-ai --function=foo example.bc

For detailed documentation, see SymAbsAI – Symbolic Abstraction + Abstract Interpretation.

Sifa – Symbolic Interpretation with Fluid Abstractions

Sifa is a symbolic-interpretation verifier with configurable abstract domains and optional SymAbs-backed reasoning.

Binary: lotus-verify-sifa Source: tools/verifier/sifa/lotus-verify-sifa.cpp

Quick Start:

./build/bin/lotus-verify-sifa program.bc
./build/bin/lotus-verify-sifa program.bc --function=foo --block=loop.header
./build/bin/lotus-verify-sifa program.bc --symabs --abstract-domain=Octagon

For detailed documentation, see Sifa Tool.

SeaHorn – Verification Framework

SeaHorn is a large-scale SMT-based verification framework built on constrained Horn clauses (CHC), symbolic execution, and abstraction-refinement.

Binaries: seahorn, seapp, seainspect Location: tools/verifier/seahorn/

Quick Start:

# Bounded model checking
./build/bin/seahorn --horn-bmc program.bc

# CHC-based verification
./build/bin/seahorn --horn-solve program.bc

For detailed documentation, see SeaHorn – Verification Framework.

SMACK – LLVM-to-Boogie Verification

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

Binaries: llvm2bpl, extern-statics Location: tools/verifier/smack/

llvm2bpl is the LLVM-to-Boogie translator and extern-statics externalizes static functions; the smack frontend script and its helpers (smack-doctor, smack-svcomp-wrapper.sh) are installed alongside them.

Build status: built only when LOTUS_ENABLE_SMACK=ON.

For detailed documentation, see SMACK Verification Frontend.

Mosaic – Theory-Modular CHC Solving

Mosaic is a theory-modular Constrained Horn Clause (CHC) solver that decomposes proof obligations into mixed-theory sub-problems (Int/BV).

Binary: lotus-verify-mosaic Location: tools/verifier/mosaic/

Quick Start:

./build/bin/lotus-verify-mosaic input.smt2
./build/bin/lotus-verify-mosaic --backend=mosaic --force-preprocess input.smt2

For detailed documentation, see Mosaic.

Horn-ICE – CHC Verification with Learning

Horn-ICE provides CHC (Constrained Horn Clause) verification with invariant learning capabilities.

Binaries: chc_verifier, hice-dt Location: third-party/horn-ice/

Usage:

# CHC verification
./build/bin/chc_verifier input.smt2

# CHC verification with learning
./build/bin/hice-dt input.smt2

Build status: built by default when LOTUS_ENABLE_HORN_ICE=ON.

For detailed documentation, see Horn-ICE – CHC Verification with Learning.