(Extended) Interval Analysis

Achim D. Brucker 🌐 and Amy Stell 🌐

January 21, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Related publications

  • A. D. Brucker, T. Cameron-Burke, and A. Stell. Formally verified interval arithmetic and its appli- cation to program verification. In 13th IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE 2024). IEEE, 2024.
  • R. E. Moore, R. B. Kearfott, and M. J. Cloud. Introduction to Interval Analysis. Society for Industrial and Applied Mathematics, USA, 2009. isbn: 0898716691.

Session Interval_Analysis