Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:abstract_interpretation [2008/04/30 10:46] vkuncak |
sav08:abstract_interpretation [2008/04/30 11:02] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Abstract Interpretation ====== | ====== Abstract Interpretation ====== | ||
| + | |||
| + | Goal: Invariant Inference by Approximation | ||
| + | |||
| + | Approximate strongest postcondition $sp$ with operator $sp\#$ whose fixedpoint e.g. has a finite height. | ||
| Let PS denote program states and $C = 2^{PS}$ denote the set of all subsets of PS, so $S \subseteq PS$ and $S \in C$ for a set of states S. We introduce an abstract analysis domain A and functions | Let PS denote program states and $C = 2^{PS}$ denote the set of all subsets of PS, so $S \subseteq PS$ and $S \in C$ for a set of states S. We introduce an abstract analysis domain A and functions | ||
| Line 56: | Line 60: | ||
| \end{eqnarray*} | \end{eqnarray*} | ||
| because of the way we defined order. | because of the way we defined order. | ||
| + | |||
| + | Consider first only a single loop. | ||
| Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$. We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop): | Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$. We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop): | ||
| Line 70: | Line 76: | ||
| * [[http://www.di.ens.fr/~cousot/COUSOTtalks/VMCAI05_TOOLS.shtml|A Tutorial Abstract Interpretation by the inventor Patrick Cousot]] | * [[http://www.di.ens.fr/~cousot/COUSOTtalks/VMCAI05_TOOLS.shtml|A Tutorial Abstract Interpretation by the inventor Patrick Cousot]] | ||
| + | * [[:sav07_lecture_7|Approximation Expressed Using Formulas]] | ||
| + | * [[Calculus of Computation Textbook]], Chapter 12 on invariant generation | ||