Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form z = x op y and use constraint propagation techniques to infer new information on the variables’ possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.

Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification / Bagnara, Roberto; Bagnara, Abramo; Biselli, Fabio; Chiari, Michele; Gori, Roberta. - In: CONSTRAINTS. - ISSN 1383-7133. - (2022). [10.1007/s10601-021-09322-9]

Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification

Roberto Bagnara;Fabio Biselli;Michele Chiari;
2022

Abstract

Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form z = x op y and use constraint propagation techniques to infer new information on the variables’ possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.
Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification / Bagnara, Roberto; Bagnara, Abramo; Biselli, Fabio; Chiari, Michele; Gori, Roberta. - In: CONSTRAINTS. - ISSN 1383-7133. - (2022). [10.1007/s10601-021-09322-9]
File in questo prodotto:
File Dimensione Formato  
BagnaraBBCG22.pdf

accesso aperto

Descrizione: Articolo principale.
Tipologia: Versione (PDF) editoriale
Licenza: Creative commons
Dimensione 5.71 MB
Formato Adobe PDF
5.71 MB Adobe PDF Visualizza/Apri
main (1).pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Creative commons
Dimensione 433.66 kB
Formato Adobe PDF
433.66 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11381/2907356
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact