SMT-based incremental bounded model-checking

SAT-based bounded model checker using interpolation-based function summaries

SAT-based bounded model checker with upgrade checking capabilities

Parallel Software Model Checker

SMT-based Bounded Model Checker for C with Function Summaries

Verifier for programs with arrays

Invariant generator for Boogie

Model checker for programs with arrays

Loop summarization based static analyzer for C programs

Constrained Horn Clause Solver

Compact and open-source SMT-solver written in C++

SAT-solver capable of proof manipulation and interpolant generation

Interpolator that supports Partial Variable Assignment Interpolants (PVAIs)