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.

PeRIPLO

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

OpenSMT

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

Loopfrog

- a loop summarization based static analyzer for C programs.

eVolCheck

- a bounded model checker with upgrade checking capabilities.

SAFARI

- a model checker for programs with arrays.

FunFrog

- a bounded model checker using interpolation-based function summaries

Synergy

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

Boppo

- a model checker for Boolean programs.

SATABS

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

Syndicate content