Non-integer arithmetic is prone to numerical errors due to the finite representation of numbers. These errors propagate, possibly non-linearly, throughout the variables of a program and can affect its control flow, altering reachability, and thus safety. We consider the problem of rigorous bit-precise numerical accuracy certification of programs in the presence of control structures and operations under fixed-point arithmetic over (non-deterministic) variables of arbitrary, mixed precision. By applying program transformation, we reduce the problem of assessing whether a given error bound can be exceeded in the initial program to a reachability problem in a bit-vector program. We implement our technique as a pre-processing module that integrates seamlessly with an existing mature BMC-based verification workflow. We present an experimental evaluation of our error certification technique on a set of arithmetic routines commonly used in the industry.

Bit-Precise Verification of Discontinuity Errors Under Fixed-Point Arithmetic

Simic S.;Tribastone M.
2021

Abstract

Non-integer arithmetic is prone to numerical errors due to the finite representation of numbers. These errors propagate, possibly non-linearly, throughout the variables of a program and can affect its control flow, altering reachability, and thus safety. We consider the problem of rigorous bit-precise numerical accuracy certification of programs in the presence of control structures and operations under fixed-point arithmetic over (non-deterministic) variables of arbitrary, mixed precision. By applying program transformation, we reduce the problem of assessing whether a given error bound can be exceeded in the initial program to a reachability problem in a bit-vector program. We implement our technique as a pre-processing module that integrates seamlessly with an existing mature BMC-based verification workflow. We present an experimental evaluation of our error certification technique on a set of arithmetic routines commonly used in the industry.
978-3-030-92123-1
978-3-030-92124-8
Bounded model checking
Control-flow
Discontinuity error
Fixed-point arithmetic
Numerical error
Program transformation
File in questo prodotto:
File Dimensione Formato  
Simić2021_Chapter_Bit-PreciseVerificationOfDisco.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Nessuna licenza
Dimensione 2.3 MB
Formato Adobe PDF
2.3 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/20.500.11771/20869
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
social impact