You are here: Home › Tools › ToolsOld

ToolsOld

  • ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement) is a model checker for C programs based on the abstraction-verification-refinement paradigm. It is used for the automatic detection of runtime errors (array out of bounds, buffer overflow, NULL pointer dereference, etc.).
    ACSAR abstracts not just states but also the state changes induced by structured program statements, including for- and while-statements. The use of such abstraction allows one to shortcut ``transfinite'' sequence of refinement steps. For more information, please contact Nassim Seghir.

  • AMTV(Automated Modular Thread Verifier) proves safety of multithreaded programs. AMTV takes a finite-state multithreaded program and a specification; it outputs either an inductive invariant that proves the property or all shortest error traces. AMTV always terminates with a definite answer. AMTV is polynomial-time on all programs with thread-modular proofs and on a class of binary mutex programs without thread-modular proofs. AMTV practically fights the state explosion problem in the number of threads, scaling, for example, up to 100 threads on the binary mutex programs. For more information, please contact Alexander Malkis.

  • Bohne is a symbolic shape analysis tool. It infers loop invariants of programs manipulating heap-allocated data structures. Bohne is integrated into the Jahob verification system. A standalone version of Bohne will be available, soon. For more information, please contact Thomas Wies.

  • Exorcise closes the gap between static analysis used in modern compilers and state of the art formal methods. It produces precise and intuitive compiler-like error messages (i.e., it never generates false alarms) and detects even sophisticated errors and certain cases of non-termination by analyzing the entire state space of the program. Exorcise detects doomed program points which are expressions or statements in a program that cannot be executed (i.e., they either crash the program or are unreachable) due to contradictions in the control flow or specification.

  • MCTA: Mcta is a model checking tool for real-time specifications modelled as timed automata. Although the tool can be used for verification, Mcta is rather optimized for falsification, i.e., detecting violations against safety properties fast and returning short error traces. Several types of traces can be generated, including an option to find a (guaranteed) shortest error trace. For more information, please contact Martin Wehrle.

  • SmtInterpol is an SMT-Solver which can compute Craig-Interpolants for the quantifier free combined theory of uninterpreted functions and linear arithmetic over rationals and integers. SmtInterpol is developed by Jochen Hoenicke and Jürgen Christ.

  • Ultimate is a model checker for Boogie programs based on abstraction-refinement loop and interpolation. The Boogie language is an intermediate language for verification. Using existing frontends like VCC or Spec-# it is possible to verify C and C# programs. In the long run Ultimate should incorporate invariant generation, termination checking, and modular verification for multi-threaded programs. For more information, please contact Jochen Hoenicke.