You are here

Our tools

Our research involves a lot of experimental evaluation. For that, we develop different tools, which can be used by other researchers as well.

Active Tools:

Model Checkers

UpProver	SMT-based incremental bounded model-checking	Github
FunFrog	SAT-based bounded model checker using interpolation-based function summaries	Github
eVolCheck	SAT-based bounded model checker with upgrade checking capabilities	Source Code
SMTS	Parallel Software Model Checker	Source Code
HiFrog	SMT-based Bounded Model Checker for C with Function Summaries	Github
Booster	Verifier for programs with arrays	More Information
Verige	Invariant generator for Boogie	More Information
SAFARI	Model checker for programs with arrays	More Information
LoopFrog	Loop summarization based static analyzer for C programs	More Information

Computational Solvers

Golem	Constrained Horn Clause Solver	Github
OpenSMT	Compact and open-source SMT-solver written in C++	Github
PeRIPLO	SAT-solver capable of proof manipulation and interpolant generation	More Information
PVAIR	Interpolator that supports Partial Variable Assignment Interpolants (PVAIs)	More Information