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
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	Award-winning 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
PyCHC	A Framework for Design and Certified Solving of CHC systems	Github
SMTS	Parallel SMT solver with Iterative Partitioning and Lemma Sharing	Github

Neural Network Analyzers

SpEXplAIn

A tool for computing space explanations of neural network classifiers

Archived tools

SMTS (old)

Parallel Software Model Checker

You are here