Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers

Reference. Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers

Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala · SMT · numerical-verification · DOI

The treatment of the axiomatic theory of floating-point numbers is out of reach of current SMT solvers, especially when it comes to automatic reasoning on approximation errors. In this paper, we describe a dedicated procedure for such a theory, which provides an interface akin to the instantiation mechanism of an SMT solver. This procedure is based on the approach of the Gappa tool: it performs saturation of consequences of the axioms, in order to refine bounds on expressions. In addition to the original approach, bounds are further refined by a constraint solver for linear arithmetic. Combined with the natural support for equalities provided by SMT solvers, our approach improves the treatment of goals coming from deductive verification of numeric programs. We have implemented it in the Alt-Ergo SMT solver.

Cite

Cite as @conchon-nd-built (helia, typst) · \cite{conchon-nd-built} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{conchon-nd-built, title={Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers}, volume={20}, ISSN={2398-7340}, url={http://dx.doi.org/10.29007/wh99}, DOI={10.29007/wh99}, booktitle={EPiC Series in Computing}, publisher={EasyChair}, author={Conchon, Sylvain and Melquiond, Guillaume and Roux, Cody and Iguernelala, Mohamed}, pages={12–1} }

hayagriva YAML (typst)

yaml · 18 lines

conchon-nd-built:
  type: article
  title: Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
  author:
  - Conchon, Sylvain
  - Melquiond, Guillaume
  - Roux, Cody
  - Iguernelala, Mohamed
  page-range: 12-1
  url: http://dx.doi.org/10.29007/wh99
  serial-number:
    doi: 10.29007/wh99
    issn: 2398-7340
  parent:
    type: proceedings
    title: EPiC Series in Computing
    publisher: EasyChair
    volume: 20

Download: conchon-nd-built.bib · conchon-nd-built.yml

Cites 14 works (0 here)

External (14)

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic (2012)
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa (2011)
Handbook of Floating-Point Arithmetic (2010)
Certification of bounds on expressions involving rounded operators (2010)
Multi-Prover Verification of Floating-Point Programs (2010)
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems (2010)
Numerical stability analysis of floating-point computations using software model checking (2010)
An SMT-LIB theory of binary floating-point arithmetic (2010)
Z3: An Efficient SMT Solver (2008)
IEEE Standard for Floating-Point Arithmetic (IEEE 754-2008) (2008)
CVC3 (2007)
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification (2007)
Alt-Ergo (tool) (2006)
Yices (tool paper) (2006)