(Extended) Interval Analysis

By Achim D. Brucker and Amy Stell.

Interval analysis (also called interval arithmetic) is a well known mathematical technique to analyse or mitigate rounding errors 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 computations stay within the hardware bounds of a given number representation.

Another application is the verification of cyber-physical systems, where a discretised implementation approximates a system described in physical quantities expressed using perfect mathematical reals, and perfect ordinary differential equations.

In this AFP entry, we formalise extended interval analysis, including the concept of inclusion isotone (or inclusion isotonic) (extended) interval analysis. The main result is the formal proof that interval-splitting converges for Lipschitz-continuous interval isotone functions. From pragmatic perspective, we provide the datatypes and theory required for integrating interval analysis into other formalisations and applications.

Please cite this work as follows:
A. D. Brucker and A. Stell, “(Extended) Interval Analysis,” Archive of Formal Proofs, Jan. 2024. https://www.isa-afp.org/entries/Interval_Analysis.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-afp-2024/

BibTeX
@Article{ brucker.ea:interval-arithmetic-afp:2024,
  author   = {Achim D. Brucker and Amy Stell},
  title    = {{(Extended)} {Interval} {Analysis}},
  journal  = {Archive of Formal Proofs},
  month    = {jan},
  year     = {2024},
  date     = {2024-01-21},
  note     = {\url{https://www.isa-afp.org/entries/Interval_Analysis.html},
              Formal proof development. 
              Author copy: \url{https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-afp-2024/}},
  issn     = {2150-914x},
  areas    = {formal methods},
  abstract = {Interval analysis (also called interval arithmetic) is a well
              known mathematical technique to analyse or mitigate rounding
              errors 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 computations stay within the hardware bounds of a
              given number representation.
              
              Another application is the verification of cyber-physical
              systems, where a discretised implementation approximates a
              system described in physical quantities expressed using
              perfect mathematical reals, and perfect ordinary differential
              equations.
              
              In this AFP entry, we formalise extended interval analysis,
              including the concept of inclusion isotone (or inclusion
              isotonic) (extended) interval analysis. The main result is the
              formal proof that interval-splitting converges for
              Lipschitz-continuous interval isotone functions. From
              pragmatic perspective, we provide the datatypes and theory
              required for integrating interval analysis into other
              formalisations and applications.},
  pdf      = {https://logicalhacking.com/publications/brucker.ea-interval-arithmetic-afp-2024/brucker.ea-interval-arithmetic-afp-2024.pdf},
}