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:55] 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 72: | 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 | ||