LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:homework11 [2008/05/15 12:58]
vkuncak
sav08:homework11 [2015/04/21 17:30] (current)
Line 33: Line 33:
  
 **Part a)** Consider [[Conjunctions of Predicates]] as abstract interpretation domain. ​ Give example showing that it need not be the case that  **Part a)** Consider [[Conjunctions of Predicates]] as abstract interpretation domain. ​ Give example showing that it need not be the case that 
-\[+\begin{equation*}
     a_1 \leq a_2 \leftrightarrow \gamma(a_1) \subseteq \gamma(a_2)     a_1 \leq a_2 \leftrightarrow \gamma(a_1) \subseteq \gamma(a_2)
-\]+\end{equation*}
  
 **Part b)** Describe how to construct from $A$ a new, smaller, lattice $B$, where the above equivalence holds. ​ Is there an algorithm to compute $B$ and the partial order on $B$ using a decision procedure for the logic of predicates? **Part b)** Describe how to construct from $A$ a new, smaller, lattice $B$, where the above equivalence holds. ​ Is there an algorithm to compute $B$ and the partial order on $B$ using a decision procedure for the logic of predicates?