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] (current) 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 | ||