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:
|
|
Constrained Horn Clause Solver |
|
|
SMT-Based incremental Bounded Model-Checking |
|
|
SMT-Based Bounded Model-Checking for C with Function Summaries. |
|
|
a compact and open-source SMT-solver written in C++. |
|
|
Parallel Software Model Checker based on PDR. |
|
|
a bounded model checker using interpolation-based function summaries. |
|
|
a SAT-solver capable of proof manipulation and interpolant generation. |
|
|
a bounded model checker with upgrade checking capabilities. |
|
|
A verifier for programs with arrays. |
|
|
An invariant generator for Boogie. |
| PVAIR |
An interpolator that supports Partial Variable Assignment Interpolants (PVAIs)
|
|
|
a model checker for programs with arrays. |
|
|
a loop summarization based static analyzer for C programs. |
Other tools:
|
|
a tool to compare effectiveness of abstraction techniques in verification of ANSI-C programs. |
|
|
a verification tool for ANSI-C and C++ programs. |
