Exploiting binary floating-point representations for constraint propagation

DOI10.1287/IJOC.2015.0663zbMATH Open1357.68010arXiv1308.3847OpenAlexW1797291051MaRDI QIDQ2806863FDOQ2806863

Matthieu Carlier, Roberto Bagnara, Arnaud Gotlieb, Roberta Gori

Publication date: 19 May 2016

Published in: INFORMS Journal on Computing (Search for Journal in Brave)

Abstract: Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations is a hot research topic. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, as constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the propagation of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers.

Full work available at URL: https://arxiv.org/abs/1308.3847

Recommendations

• scientific article; zbMATH DE number 2084728
• Sharpening constraint programming approaches for bit-vector theory
• Propagation based local search for bit-precise reasoning
• scientific article; zbMATH DE number 2243409
• Enhancing numerical constraint propagation using multiple inclusion representations
• Improving linear constraint propagation by changing constraint representation
• Principles and Practice of Constraint Programming – CP 2004

zbMATH Keywords

testingsoftware verificationconstraint solvingfloating-point numbers

Mathematics Subject Classification ID

Reliability, testing and fault tolerance of networks and computer systems (68M15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Numerical algorithms for computer arithmetic, etc. (65Y04)

Cites Work

• ICOS: a branch and bound based solver for rigorous global optimization
• Algorithm 852
• Contractor programming
• Tools and Algorithms for the Construction and Analysis of Systems
• Exploiting binary floating-point representations for constraint propagation
• Numeric Bounds Analysis with Conflict-Driven Learning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theoretical Analysis of Local Search in Software Testing
• An Abstract Interpretation Based Combinator for Modelling While Loops in Constraint Programming
• Standardization and Testing of Mathematical Functions

Cited In (8)

• Solving the generalized mask constraint for test generation of binary floating point add operation.
• Exploiting binary floating-point representations for constraint propagation
• Finding normal binary floating-point factors efficiently
• Deciding floating-point logic with abstract conflict driven clause learning
• Title not available (Why is that?)
• Deferring Dag Construction by Storing Sums of Floats Speeds-Up Exact Decision Computations Based on Expression Dags
• Correct approximation of IEEE 754 floating-point arithmetic for program verification
• Enhancing numerical constraint propagation using multiple inclusion representations

Uses Software

• ICOS
• RealPaver
• GATeL
• DART
• CBMC
• FloPSy
• AUSTIN

This page was built for publication: Exploiting binary floating-point representations for constraint propagation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2806863)