Open Hub
Black Duck Open Hub

Tags : Browse Projects

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

DIVINE

Compare

  Analyzed about 1 month 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++.

184K lines of code

11 current contributors

almost 2 years since last commit

3 users on Open Hub

Activity Not Available
0.0
 
0 Reviews
I Use This
Mostly written in C++
Licenses: bsd_2clau...
Tags c++11 llvm ltl model_checking software_verification verification

CPAchecker

Compare

  Analyzed about 19 hours ago

CPAchecker is a tool for configurable software verification. For more information on the CPAchecker project, please visit the CPAchecker Project Home Page.

400K lines of code

23 current contributors

1 day since last commit

0 users on Open Hub

High Activity
0.0
 
0 Reviews
I Use This
Mostly written in Java
Licenses: apache_2
Tags model_checking program_analysis software_verification static_analysis verification

Set Decision Diagrams and ITS tools

Compare

  Analyzed about 1 hour 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]

677K lines of code

2 current contributors

8 days since last commit

0 users on Open Hub

Moderate Activity
0.0
 
0 Reviews
I Use This
Mostly written in Java
Licenses: gpl
Tags ctl ltl model_checking petri_nets verification

Klever

Compare

  Analyzed about 10 hours ago

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]

268K lines of code

6 current contributors

2 days since last commit

0 users on Open Hub

Low Activity
0.0
 
0 Reviews
I Use This
Mostly written in JavaScript
Licenses: apache_v2
Tags c formal_methods formalmethods model_checking modelchecking software_verification specification static_analysis verification