# Interval Analysis and Widening

Interval analysis domain, for each program point, maps each program variable to an interval.

Interval bounds may be and . Interval represents no constraints.

Analysis domain has elements where denotes the set of such intervals.

How to interpret a command

for some operation ?

What does the lattice of intervals look like?

Height of lattice of one interval for 64-bit integers:

If we have variables in program and program points, height of lattice for the analysis domain is times larger.

For unbounded integers, lattice is unbounded.

How to guarantee termination?

Widening technique: if we do not seem to be converging, make a “jump”.

Finite set of “jump points” (e.g. set of all integer constants in the program)

In fixpoint computation, compose with function

Approaches:

- always apply widening (we will assume this)
- iterate a few times with only (without using ), if not a fixpoint at this program point, then widen.
- this is not monotonic: if you start at fixpoint, it converges, if start below, can jump over fixpoint

Standard iteration:

Widening:

Here, for all by definition of

Narrowing: after finding fixpoint of , apply to improve precision.

Observation: if and are -continuous functions and for all , then narrowing will improve the result, that is, if and , then and