Our tools

 

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

Active Tools:

 

HiFrog

 

SMT-Based Bounded Model-Checking for C with Function Summaries.

 

OpenSMT2

 

a compact and open-source SMT-solver written in C++.

 

FunFrog

 

a bounded model checker using interpolation-based function summaries.

 

PeRIPLO

 

a SAT-solver capable of proof manipulation and interpolant generation.

 

eVolCheck

 

a bounded model checker with upgrade checking capabilities.

 

Booster

 

A verifier for programs with arrays.

 

Verige

 

An invariant generator for Boogie.

PVAIR

 

An interpolator that supports Partial Variable Assignment Interpolants (PVAIs)

 

 

SAFARI

 

a model checker for programs with arrays.

 

Loopfrog

 

a loop summarization based static analyzer for C programs.

 

Other tools:

 

Synergy

 

a tool to compare effectiveness of abstraction techniques in verification of ANSI-C programs.

 

SATABS

 

a verification tool for ANSI-C and C++ programs.