Cited in
(45)- Formal analysis of the compact position reporting algorithm
- A validated real function calculus
- Validating QBF Validity in HOL4
- On large families of subsets of the set of the integers not exceeding \(N\)
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Axiomatic reals and certified efficient exact real computation
- Polynomial function intervals for floating-point software verification
- Elementary functions. Algorithms and implementation
- CADNA
- RealLib
- ACSL
- RealPaver
- core 2
- SLEEF
- Ariadne
- C-CoRN
- Flocq
- iRRAM
- PolyPaver
- Squolem
- Sollya
- Manip
- PVSio
- ASTREE
- FloPoCo
- DyTa
- SONOLAR
- UppSAT
- XSat
- Coq Interval
- PRECiSA
- Daisy
- CoVEGI
- Trusting computations: a mechanized proof from partial differential equations to actual program
- Exploring approximations for floating-point arithmetic using UppSAT
- FPTaylor
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- An approximation framework for solvers and decision procedures
- Formalization of Bernstein polynomials and applications to global optimization
- ReproBLAS
- Metalibm: a mathematical functions code generator
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
This page was built for software: Gappa
