Gappa
From MaRDI portal
swMATH4885MaRDI QIDQ17037FDOQ17037
Author name not available (Why is that?)
Official website: https://gappa.gitlabpages.inria.fr
Source code repository: https://gitlab.inria.fr/gappa/gappa
Cited In (44)
- FPTaylor
- 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
- Elementary functions. Algorithms and implementation
- Polynomial function intervals for floating-point software verification
- Trusting computations: a mechanized proof from partial differential equations to actual program
- CADNA
- ACSL
- RealPaver
- core 2
- SLEEF
- Ariadne
- C-CoRN
- Flocq
- iRRAM
- PolyPaver
- Squolem
- Sollya
- Manip
- PVSio
- ASTREE
- FloPoCo
- DyTa
- SONOLAR
- UppSAT
- XSat
- Coq Interval
- Exploring approximations for floating-point arithmetic using UppSAT
- PRECiSA
- Daisy
- CoVEGI
- 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
