# Octagons and Relational Analyses

Intervals track possible values for each variable independently.

More complex analyses are relational: they track relations between different variables.

Example of usefulness: prove in this program:

X := 10
Y := 0
while X >= 0 {
X := X-1
if random() { Y = Y+1 }
}

What would interval analysis compute? At iteration , we have , . Although stabilizes, the interval for does not converge. We must widen and obtain .

What loop invariant does proof of need?

Note: relational analyses can also track changes of variables. If we automatically insert at the beginning of each procedure

x0 = x

for each variable x, then tracking relation between x0 and x tracks the changes to x since the beginning of procedure.

Example: means the value only increases.

## Octagon Domain

For each pair of variables , , potentially track constraints of the form for some constant .

It is a simpler and more efficient version of polyhedral domain, where constraints are general systems of linear equations of the form for some matrix and vector .

Polyhedral domain uses the theory of linear arithmetic, whereas octagon domain uses theory of different logic, which is simpler and allows operations to be implemented using graph algorithms.