Formally Verified Interval Arithmetic and Its Application to Program Verification

By Achim D. Brucker, Teddy Cameron-Burke, and Amy Stell.

Interval arithmetic is a well known mathematical technique to analyse or mitigate rounding or measurement errors. Thus, it is promising to integrate interval analysis into program verification environments. Such an integration is not only useful for the verification of numerical algorithms: the need to ensure that computations stay within certain bounds is common. For example, to show that arithmetic computations stay within the hardware bounds of a given number representation. We present a formalisation of (extended) interval arithmetic in Isabelle/HOL, including the concept of inclusion isotone (extended) interval analysis. The main result of this part is the formal proof that interval-splitting converges for Lipschitz-continuous interval isotone functions. We also show how interval types can be used for verifying programs in a C-like programming language.

Keywords:
Extended Interval Analysis, Program Verification, Formalising Math- ematics, Isabelle/HOL

Supplementary material:
[  Formalization  ]

Please cite this work as follows:
A. D. Brucker, T. Cameron-Burke, and A. Stell, “Formally verified interval arithmetic and its application to program verification,” 2024. doi: 10.1145/3644033.3644370. Author copy: https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-2024/

BibTeX
@InProceedings{ brucker.ea:interval-arithmetic:2024,
  author          = {Achim D. Brucker and Teddy Cameron-Burke and Amy Stell},
  title           = {Formally Verified Interval Arithmetic and Its Application to
                     Program Verification},
  booktitle       = {13th {IEEE/ACM} International Conference on Formal Methods in
                     Software Engineering (FormaliSE 2024)},
  pages           = {},
  publisher       = {ACM},
  year            = {2024},
  doi             = {10.1145/3644033.3644370},
  keywords        = {Extended Interval Analysis, Program Verification, Formalising
                     Math- ematics, Isabelle/HOL},
  location        = {Lisbon, Portugal},
  conf_date       = {April 14-15, 2024},
  supplabel01     = {Formalization},
  supplementary01 = {},
  language        = {english},
  areas           = {formal methods, software engineering},
  abstract        = {Interval arithmetic is a well known mathematical technique to
                     analyse or mitigate rounding or measurement errors. Thus, it
                     is promising to integrate interval analysis into program
                     verification environments. Such an integration is not only
                     useful for the verification of numerical algorithms: the need
                     to ensure that computations stay within certain bounds is
                     common. For example, to show that arithmetic computations stay
                     within the hardware bounds of a given number representation.
                     We present a formalisation of (extended) interval arithmetic
                     in Isabelle/HOL, including the concept of inclusion isotone
                     (extended) interval analysis. The main result of this part is
                     the formal proof that interval-splitting converges for
                     Lipschitz-continuous interval isotone functions. We also show
                     how interval types can be used for verifying programs in a
                     C-like programming language.},
  note            = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-2024/}},
  pdf             = {https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-2024/brucker.ea-interval-arithmetic-2024.pdf},
}