Differences

This shows you the differences between two versions of the page.

--- sav08:conjunctions_of_predicates [2008/05/08 12:46]
vkuncak
+++ sav08:conjunctions_of_predicates [2008/05/08 12:55]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Abstract Interpretation with Conjunctions of Predicates ======
-Parameters: a finite set of formulas ${\cal P} = P_1,\ldots,P_n$ in program variables.
+Parameters: a finite set of formulas ${\cal P} = \{ P_0, P_1,\ldots,P_n\}$ in program variables.  Suppose $P_0$ is the predicate 'false'.
-for $a \in A$ we have $a \subseteq {\cal P}$
+Let $A = 2^{\cal P}$, so for $a \in A$ we have $a \subseteq {\cal P}$.
-Using [[Abstract Interpretation Recipe]] we construct:
+We design analysis using [[Abstract Interpretation Recipe]].
-  * abstract domain: truth values of predicates
-  * concretization function: states given by truth values
-  * abstraction function
-  * best abstract post for simple programming language
-Finite lattice.
+Define a syntactic order on $(A,\le)$
+Finite lattice.
+Defining $\gamma$.
+Defining $\alpha$.
+Is it the case that $\alpha(\gamma(a))=a$?
-Two different orders.