Select a tag to browse associated projects and drill deeper into the tag cloud.
Spot
Claimed by EPITA Research and Developm... Analyzed 2 months ago
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.
Licenses:
gpl3_or_l...
DIVINE
Analyzed 2 months ago
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++.
Licenses:
bsd_2clau...
Set Decision Diagrams and ITS tools
S
Analyzed 2 months ago
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
ultimate
Analyzed 2 months ago
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
Licenses:
lgplv3-st...