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++.
We provide a collection of approaches, tools, and research results which are related to behavioural aspects of service technology such as service composition, discovery, mediation, substitution, and others. This technology is the result of joint research efforts of the theory of programming groups
... [More] at Humboldt-Universität zu Berlin, the University of Rostock, the Technische Universiteit Eindhoven, and several cooperation partners. [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]
Klever is a software verification framework that aims at automated checking of programs developed in the GNU C programming language against a variety of requirements using software model checkers (automatic software verification tools) implementing such methods of thorough static analysis as Bounded
... [More] Model Checking and Counterexample-Guided Abstraction Refinement. Software model checking allows finding faults that can be hardly detected by other software quality assurance techniques like code review, testing and static analysis. In addition, it is capable to prove formal correctness of programs checked against particular requirements under certain assumptions. [Less]