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 metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01795760
Contributor : Zakaria Chihani <>
Submitted on : Friday, May 18, 2018 - 4:53:22 PM
Last modification on : Thursday, February 7, 2019 - 2:38:16 PM
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

Collections

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

106

Files downloads

49