Differences

This shows you the differences between two versions of the page.

--- sav08:octagons_and_relational_analysis [2008/05/20 16:23]
vkuncak created
+++ sav08:octagons_and_relational_analysis [2008/05/20 23:55]
vkuncak
@@ Line 1: / Line 1: @@
 ====== 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:
+<code>
+X := 10
+Y := 0
+while X >= 0 {
+  X := X-1
+  if random() { Y = Y+1 }
+}
+</code>
+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? ++|$X + Y \le 10$.  Note it relates values of $X$ and $Y$, interval analysis cannot compute it. ++
+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
+\[
+    \pm X \pm Y \le c
+\]
+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 =====
   * [[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|Octagons paper]] contains motivation for relational analysis