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?
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
- 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
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