Software Engineering
Document Actions

Tools

  • AMTV: Automated Modular Thread Verifier. AMTV 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.

  • ACSAR (Automatic Checker of Safety properties based on Abstraction Refinement)
    ACSAR 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.

  • 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.

  • 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 is an extension to Boogie that allows to detect doomed program points in .Net programs.

  • 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.

  • 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. Read more.