LARA

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 $Y \le 11$ 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 $k$, we have $X \in [10-k,10]$, $Y \in [0,k]$. Although $X \in [0,10]$ stabilizes, the interval for $Y$ does not converge. We must widen and obtain $[0,+\infty]$.

What loop invariant does proof of $Y \le 11$ 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: $x0 \le x$ means the value only increases.

Octagon Domain

For each pair of variables $X$, $Y$, potentially track constraints of the form

\begin{equation*} \pm X \pm Y \le c \end{equation*}

for some constant $c$.

It is a simpler and more efficient version of polyhedral domain, where constraints are general systems of linear equations of the form $A \vec x \le \vec b$ for some matrix $A$ and vector $\vec b$.

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