# 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.

## Reference

- A. Mine: The Octagon Abstract Domain (has 90 pages but is easy to read)