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

FunFrog

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

eVolCheck

SAT-based bounded model checker with upgrade checking capabilities

SMTS

Parallel Software Model Checker

HiFrog

SMT-based Bounded Model Checker for C with Function Summaries

Booster

Verifier for programs with arrays

Verige

Invariant generator for Boogie

SAFARI

Model checker for programs with arrays

LoopFrog

Loop summarization based static analyzer for C programs

Computational Solvers

Golem

Constrained Horn Clause Solver

OpenSMT

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

PeRIPLO

SAT-solver capable of proof manipulation and interpolant generation

PVAIR

Interpolator that supports Partial Variable Assignment Interpolants (PVAIs)