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 [2009/04/01 03:21]
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'.
-Let $A = 2^{\cal P}$, so 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}$.
 We design analysis using [[Abstract Interpretation Recipe]].
-Finite lattice.
+Define a syntactic order on $(A,\le)$
-Two different orders.
+Finite lattice.
+Defining $\gamma$.
+Defining $\alpha$.
+Is it the case that $\alpha(\gamma(a))=a$?
+Using a theorem prover to compute $sp^\#$.