Gappa

swMATH4885MaRDI QIDQ17037

No author found.

Described by source

• Certification of bounds on expressions involving rounded operators

Related Items (18)

Certifying the Floating-Point Implementation of an Elementary Function Using Gappa ⋮ An approximation framework for solvers and decision procedures ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Axiomatic reals and certified efficient exact real computation ⋮ Elementary Functions ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ A validated real function calculus ⋮ Polynomial function intervals for floating-point software verification ⋮ Unnamed Item ⋮ Formal analysis of the compact position reporting algorithm ⋮ On large families of subsets of the set of the integers not exceeding \(N\) ⋮ Exploring approximations for floating-point arithmetic using UppSAT ⋮ Validating QBF Validity in HOL4 ⋮ Combining Coq and Gappa for Certifying Floating-Point Programs ⋮ Formalization of Bernstein polynomials and applications to global optimization ⋮ Metalibm: A Mathematical Functions Code Generator

This page was built for software: Gappa