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