Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav07_lecture_10_skeleton [2007/04/18 15:33] vkuncak created |
sav07_lecture_10_skeleton [2007/04/19 11:53] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Lecture 10 Skeleton ====== | ====== Lecture 10 Skeleton ====== | ||
- | Gues lecture by Andrey Rybalchenko: | + | Guest lecture by Andrey Rybalchenko: |
* [[http://www.mpi-inf.mpg.de/~rybal|Andrey's web page with links to papers]] | * [[http://www.mpi-inf.mpg.de/~rybal|Andrey's web page with links to papers]] | ||
* [[http://www.mpi-inf.mpg.de/~rybal/papers|Links to paper pdfs]] | * [[http://www.mpi-inf.mpg.de/~rybal/papers|Links to paper pdfs]] | ||
+ | |||
+ | |||
+ | ===== ASTREE Static Analyzer ===== | ||
+ | |||
+ | === 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]] | ||