Spot is a C++14 library for manipulating omega-automata and LTL/PSL formulas. It offers a set of bricks to experiment with and develop your own model checker, or do other formulas/automata transformations. It comes with a dozen command-line utilities, and Python bindings.
DIVINE is a modern explicit-state model checker. Building on high-performance algorithms and data structures, it offers unparalleled versatility, scaling from a typical developer’s laptop, up to a high-end compute cluster. What more, it can verify a wide range of languages, including C and C++.
The rtl2ba tool translates formulas of the linear-time temporal logic RTL into Büchi automata. The prominent linear-time logic LTL and the linear-time cores of the IEEE standardized logics SVA, and PSL are fragments of RTL. The output of rtl2ba can be used in the symblic model checker NuSMV. For
... [More] further information see the README.TXT file in the package. [Less]
libDDD is C++ library for manipulation of decision diagrams, both Data Decision Diagrams which are integer valued and Hierarchical Set Decision Diagrams.
ITS-tools is a multi-solution, mutli formalism model-checking toolsuite.
libITS leverages libDDD to offer a generic symbolic model-checking
... [More] kernel with high expressivity, as featured by Guarded Action Language.
CTL and LTL model-checking are built on top of libITS.
A user friendly eclipse front end with support for Promela, Divine language, Petri nets, Timed Automata and GAL. [Less]
Ultimate is a program analysis framework. Ultimate consists of several plugins that perform steps of a program analysis, e.g., parsing source code, transforming programs from one representation to another, or analyzing programs. Toolchains of these plugins can perform complex tasks, e.g., verify
... [More] that a C program fulfills a given specification. [Less]