Gappa

swMATH4885MaRDI QIDQ17037FDOQ17037

Author name not available (Why is that?)

Described by source

• Certification of bounds on expressions involving rounded operators

Cited In (18)

• Title not available (Why is that?)
• Formal analysis of the compact position reporting algorithm
• A validated real function calculus
• Metalibm: A Mathematical Functions Code Generator
• 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
• 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
• Trusting computations: a mechanized proof from partial differential equations to actual program
• Exploring approximations for floating-point arithmetic using UppSAT
• 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
• Elementary Functions
• Formal verification of numerical programs: from C annotated programs to mechanical proofs

This page was built for software: Gappa