Correct approximation of IEEE 754 floating-point arithmetic for program verification

DOI10.1007/s10601-021-09322-9zbMath1490.68078arXiv1903.06119OpenAlexW2922191282MaRDI QIDQ2152274

Abramo Bagnara, Fabio Biselli, Roberta Gori, Roberto Bagnara, Michele Chiari

Publication date: 7 July 2022

Published in: Constraints (Search for Journal in Brave)

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

zbMATH Keywords

constraint propagationconstraint satisfaction problemconstraint solvingprogram verificationfiltering algorithmsymbolic executionfloating point

Mathematics Subject Classification ID

Roundoff error (65G50) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• z3
• CVC4
• MathSAT5

Cites Work

• Deciding floating-point logic with abstract conflict driven clause learning
• Super-fast validated solution of linear systems
• Accurate solution of dense linear systems. II: Algorithms using directed rounding
• Optimal inverse projection of floating-point addition
• Underflow revisited
• Exploiting Binary Floating-Point Representations for Constraint Propagation
• Automatic detection of floating-point exceptions
• Satisfiability Modulo Theories
• Symbolic execution and program testing
• On the Computation of Correctly Rounded Sums
• Programming Languages and Systems
• The MathSAT5 SMT Solver
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Correct approximation of IEEE 754 floating-point arithmetic for program verification