Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Last revision Both sides next revision | ||
|
sav07_lecture_11_skeleton [2007/04/25 08:54] vkuncak created |
sav07_lecture_11_skeleton [2007/04/25 15:55] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| + | ===== Modular analysis of procedures ===== | ||
| + | |||
| + | Inlining specifications. Last part of [[SAV07 Homework 4]]. | ||
| + | |||
| + | Postconditions that refer to values of variables in the precondition. | ||
| + | |||
| + | The meaning of modifies clauses. | ||
| + | |||
| ===== ASTREE Static Analyzer ===== | ===== ASTREE Static Analyzer ===== | ||
| + | |||
| + | === The Octagon Abstract Domain === | ||
| + | |||
| + | [[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|Link to paper]] | ||
| + | |||
| === A Static Analyzer for Large Safety-Critical Software === | === A Static Analyzer for Large Safety-Critical Software === | ||
| Line 9: | Line 22: | ||
| * 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 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 | * 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 === | === Combination of Abstractions in the ASTRÉE Static Analyzer === | ||