Skip to Main content Skip to Navigation
Conference papers

Real Behavior of Floating Point Numbers

Bruno Marre 1, 2 François Bobot 2, 1 Zakaria Chihani 2, 1
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : We present an efficient constraint programming (CP) approach to the SMTLIB theory of quantifier-free floating-point arithmetic (QF FP). We rely on dense interreduction between many domain representations to greatly reduce the search space. We compare our tool to current state-of-the-art SMT solvers and show that it is consistently better on large problems involving non-linear arithmetic operations (for which bit-blasting techniques tend to scale badly). Our results emphasize the importance of the conservation of the high-level structure of the original problems.
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01795760
Contributor : Zakaria Chihani Connect in order to contact the contributor
Submitted on : Friday, May 18, 2018 - 4:53:22 PM
Last modification on : Saturday, June 26, 2021 - 3:42:19 AM
Long-term archiving on: : Tuesday, September 25, 2018 - 12:46:33 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01795760, version 1

Citation

Bruno Marre, François Bobot, Zakaria Chihani. Real Behavior of Floating Point Numbers. The SMT Workshop, SMT 2017, 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany. ⟨cea-01795760⟩

Share

Metrics

Record views

207

Files downloads

156