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

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

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

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 propagation; constraint satisfaction problem; constraint solving; program verification; filtering algorithm; symbolic execution; floating point

Mathematics Subject Classification ID

65G50: Roundoff error

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

• z3
• CVC4
• MathSAT5