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)