Tags : Browse Projects

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.

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]

SPIN is a model checker for verifying the correctness of concurrent software models. Systems to be verified are described in Promela (Process Meta Language), which supports modeling of asynchronous distributed algorithms as non-deterministic automata (SPIN stands for "Simple Promela Interpreter").