LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav07_lecture_9_skeleton [2007/04/17 19:58]
vkuncak
sav07_lecture_9_skeleton [2007/04/19 11:53]
vkuncak
Line 32: Line 32:
 \end{equation*} \end{equation*}
 where $a^1,​\ldots,​a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph). where $a^1,​\ldots,​a^n$ are variables ranging over a lattice $A$ (one for each control-flow graph node), and $f_k$ are monotonic functions on $A$ (one for each edge in the control-flow graph).
 +
  
  
Line 84: Line 85:
 === Narrowing === === Narrowing ===
  
-===== ASTREE Static Analyzer ​===== +=== Reduced product ​===
- +
-=== A Static Analyzer for Large Safety-Critical Software === +
- +
-[[http://​www.di.ens.fr/​~cousot/​COUSOTpapers/​PLDI03.shtml|Link to paper]] +
- +
-Section 5.4: A remark on notation: +
-  * if $\rho$ denotes the state and $S$ is a deterministic statement, then $[\![S]\!]^s(\rho)$ represents the new state after executing the statement; the relation corresponding to statement semantics would be $\{(S,​[\![S]\!]^s(\rho)) \mid \rho \mbox{ is a state, mapping variables to their values \}$. +
-  * this function is extended to map sets of states to sets of states, which gives function mapping $E$ to $[\![S]\!]^c(E)$ and is what we called strongest postcondition $sp(S,​E)$. +
-  * this is abstracted to abstract domain +
- +
-=== The Octagon Abstract Domain === +
- +
-[[http://​www.di.ens.fr/​~mine/​publi/​article-mine-HOSC06.pdf|Link to paper]] +
- +
-=== Combination of Abstractions in the ASTRÉE Static Analyzer === +
- +
-  * [[http://​www.di.ens.fr/​~cousot/​COUSOTpapers/​ASIAN06.shtml|Link to paper]]+