Tags : Browse Projects

Select a tag to browse associated projects and drill deeper into the tag cloud.

Spot

Compare

Claimed by EPITA Research and Developm... Analyzed 4 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.

233K lines of code

3 current contributors

4 months since last commit

4 users on Open Hub

Activity Not Available
5.0
 
I Use This

DIVINE

Compare

  Analyzed 5 months ago

DIVINE is a modern explicit-state model checker. Building on high­-per­for­mance algorithms and data structures, it offers unparalleled versatility, sca­ling 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++.

151K lines of code

11 current contributors

over 1 year since last commit

3 users on Open Hub

Activity Not Available
0.0
 
I Use This

rtl2ba

Compare

  No analysis available

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]

0 lines of code

0 current contributors

0 since last commit

0 users on Open Hub

Activity Not Available
0.0
 
I Use This
Mostly written in language not available
Licenses: bsd

Set Decision Diagrams and ITS tools

Compare

  Analyzed 1 day 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 ... [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]

684K lines of code

2 current contributors

6 days since last commit

0 users on Open Hub

High Activity
0.0
 
I Use This

ultimate

Compare

  Analyzed 30 minutes 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 ... [More] that a C program fulfills a given specification. [Less]

5.78M lines of code

26 current contributors

about 23 hours since last commit

0 users on Open Hub

Very High Activity
0.0
 
I Use This