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. |
The Lab is funded by Swiss National Science Foundation, Foundation Tasso, Hasler Foundation, EU-COST initiative and EU FP7/Pincette.
