Tags : Browse Projects

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

Gappa

Compare

  No analysis available

The Gappa tool helps developers to verify arithmetic properties on their numerical programs (either floating-point or fixed-point computations). It can also generate formal proofs of the properties for extra confidence. It has been successfully used with several projects, e.g. for writing some ... [More] robust floating-point filters of CGAL and for certifying the elementary functions of CRlibm. [Less]

0 lines of code

2 current contributors

0 since last commit

3 users on Open Hub

Activity Not Available
5.0
 
I Use This
Mostly written in language not available
Licenses: gpl

CVC4

Compare

  Analyzed about 6 hours ago

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

384K lines of code

16 current contributors

2 days since last commit

1 users on Open Hub

High Activity
5.0
 
I Use This

Hets - the Heterogenous Toolset

Compare

  Analyzed about 23 hours ago

Hets is a parsing, static analysis and proof management tool combining various tools for different specification languages, thus providing a tool for the heterogeneous specification language HetCASL. The structuring constructs of this language are those of CASL, plus some new heterogeneous ... [More] constructs for indicating the language and for language translations. Hence, Hets is based on a graph of logics and languages. [Less]

277K lines of code

0 current contributors

almost 10 years since last commit

0 users on Open Hub

Inactive
0.0
 
I Use This

ScavengerProver

Compare

  Analyzed about 1 hour ago

Scavenger is an automated theorem prover based on the new conflict resolution calculus, which lifts some aspects of the conflict-drive clause learning approach used by sat-solvers to logics with quantifiers.

5.2K lines of code

0 current contributors

about 3 years since last commit

0 users on Open Hub

Inactive
0.0
 
I Use This
Licenses: No declared licenses