package coq-vcfloat
VCFloat: Floating Point Round-off Error Analysis
Install
Dune Dependency
Authors
Maintainers
Sources
v2.3.tar.gz
sha256=daa5a26b65c086eb9014704f53f319594b9348c77d1add2b94437771ecd69ae0
Description
VCFloat is a tool for Coq proofs about floating-point round-off error.
Tags
date:2025-02-10 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloatPublished: 10 Feb 2025
Dependencies (5)
- coq-bignums
-
coq-compcert
>= "3.15" -
coq-interval
>= "4.10.0" -
coq-flocq
>= "4.1.4" & < "5.0" -
coq
>= "8.19" & < "8.21~"
Dev Dependencies
None
Used by (2)
-
coq-vst
>= "3.1beta" -
coq-vst-lib
!= "2.13"
Conflicts
None
On This Page