Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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 numerical programs. We have implemented it in the Alt-Ergo SMT solver.
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-01785166
Contributor : Guillaume Melquiond <>
Submitted on : Friday, May 4, 2018 - 10:42:56 AM
Last modification on : Wednesday, September 16, 2020 - 5:28:17 PM
Long-term archiving on: : Monday, September 24, 2018 - 8:53:51 PM

File

article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01785166, version 1

Collections

Citation

Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala. Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. 10th International Workshop on Satisfiability Modulo Theories, Jun 2012, Manchester, United Kingdom. pp.12-21. ⟨hal-01785166⟩

Share

Metrics

Record views

308

Files downloads

352