Software
- Model Checkers
-
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
Model checker for programs with arrays
Loop summarization based static analyzer for C programs
- Computational Solvers
-
Constrained Horn Clause Solver
Compact and open-source SMT-solver written in C++
SAT-solver capable of proof manipulation and interpolant generation
PVAIR Interpolator that supports Partial Variable Assignment Interpolants (PVAIs)
|