LARA

Differences

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

Link to this comparison view

sav08:octagons_and_relational_analysis [2008/05/20 23:56]
vkuncak
sav08:octagons_and_relational_analysis [2015/04/21 17:30]
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]] has 90 pages but is easy to read