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.

In this paper, 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. Moreover, we show how interval types can be used for verifying programs in a C-like programming language.