Differences

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

--- sav07_lecture_9_skeleton [2007/04/16 15:31]
vkuncak
+++ sav07_lecture_9_skeleton [2007/04/17 15:15]
vkuncak
@@ Line 78: / Line 78: @@
   * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml|Abstract interpretation]]
   * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL79.shtml|Systematic Design of Program Analysis Frameworks]]
 ===== ASTREE Static Analyzer =====
-  * [[http://www.di.ens.fr/~cousot/COUSOTpapers/PLDI03.shtml|A Static Analyzer for Large Safety-Critical Software]]
+=== A Static Analyzer for Large Safety-Critical Software ===
-  * [[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|The Octagon Abstract Domain]]
-  * [[http://www.di.ens.fr/~cousot/COUSOTpapers/ASIAN06.shtml|Combination of Abstractions in the ASTRÉE Static Analyzer]]
+[[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]]