{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T11:05:21Z","timestamp":1746097521506},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The treatment of the axiomatic theory of floating-point numbers is<\/jats:p><jats:p>out of reach of current SMT solvers, especially when it comes to<\/jats:p><jats:p>automatic reasoning on approximation errors. In this paper, we<\/jats:p><jats:p>describe a dedicated procedure for such a theory, which provides an<\/jats:p><jats:p>interface akin to the instantiation mechanism of an SMT solver.<\/jats:p><jats:p>This procedure is based on the approach of the Gappa tool: it<\/jats:p><jats:p>performs saturation of consequences of the axioms, in order to<\/jats:p><jats:p>refine bounds on expressions. In addition to the original approach,<\/jats:p><jats:p>bounds are further refined by a constraint solver for linear<\/jats:p><jats:p>arithmetic. Combined with the natural support for equalities<\/jats:p><jats:p>provided by SMT solvers, our approach improves the treatment of<\/jats:p><jats:p>goals coming from deductive verification of numeric programs. We<\/jats:p><jats:p>have implemented it in the Alt-Ergo SMT solver.<\/jats:p>","DOI":"10.29007\/wh99","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:11Z","timestamp":1516730351000},"page":"12-1","source":"Crossref","is-referenced-by-count":2,"title":["Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers"],"prefix":"10.29007","volume":"20","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cody","family":"Roux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Iguernelala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"SMT 2012. 10th International Workshop on Satisfiability Modulo Theories"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:15Z","timestamp":1516730355000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/KH27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/wh99","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}