Managed Projects

Gappa

  Analyzed about 5 hours ago

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]

25.8K lines of code

2 current contributors

almost 2 years since last commit

3 users on Open Hub

Very Low Activity
5.0
 
I Use This

Remake

  Analyzed about 14 hours ago

Remake is a build system that provides a Make-compatible rule-based syntax while supporting dynamic dependencies à la Redo. Its code is portable yet fits into a single file, so as to be easily shippable with any project.

2.27K lines of code

1 current contributors

about 2 months since last commit

1 users on Open Hub

Very Low Activity
0.0
 
I Use This

Flocq

  Analyzed 2 days ago

Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.

35.7K lines of code

0 current contributors

over 3 years since last commit

0 users on Open Hub

Inactive
0.0
 
I Use This

Interval Package for Coq

  Analyzed about 18 hours ago

This library provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

30.1K lines of code

0 current contributors

over 2 years since last commit

0 users on Open Hub

Inactive
0.0
 
I Use This

Coquelicot

  Analyzed about 17 hours ago

The Coquelicot project aims at designing a modern formalization of classical real numbers for the Coq proof assistant.

40.3K lines of code

1 current contributors

almost 2 years since last commit

0 users on Open Hub

Very Low Activity
0.0
 
I Use This