Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
sav08:homework11 [2008/05/08 18:50] vkuncak created |
sav08:homework11 [2008/05/08 18:54] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Homework 11, Due May 14 ====== | ====== Homework 11, Due May 14 ====== | ||
+ | |||
+ | ===== Problem 0 ===== | ||
+ | |||
+ | Prepare a 5-10 minute update on your project progress to present it on May 15 in exercises. | ||
===== Problem 1 ===== | ===== Problem 1 ===== | ||
Line 26: | Line 30: | ||
===== Problem 2 ===== | ===== Problem 2 ===== | ||
- | Suppose you are given a set of predicates $P_0,P_1,\ldots,P_n$ in a decidable theory of first-order logic (for example, combination of uninterpreted function symbols with integer linear arithmetic) where $P_0$ is the predicate 'false'. | + | Suppose you are given a set of predicates ${\cap P} = \{P_0,P_1,\ldots,P_n\}$ in a decidable theory of first-order logic (for example, combination of uninterpreted function symbols with integer linear arithmetic) where $P_0$ is the predicate 'false'. |
**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 | ||
Line 35: | Line 39: | ||
**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? | ||
- | **Part c)** Suppose that, for the same set of predicates, we use lattice $A$ and lattice $B$ to compute the fixpoints $g_A$ and $g_B$ of the function $F^{#}$ from [[Abstract Interpretation Recipe]]. What can you say about | + | **Part c)** Suppose that, for the same set of predicates, we use lattice $A$ and lattice $B$ to compute the fixpoints $g_A$ and $g_B$ of the function $F^{\#}$ from [[Abstract Interpretation Recipe]]. What can you say about |
- | * the comparison of numbers of iterations needed to compute the fixpoint $g_A$ and $g_B$ (is one always less than equal to the other, strictly less, for various sets of predicates) | + | * the comparison of numbers of iterations needed to compute the fixpoint $g_A$ and $g_B$ (is one always less than the other, can they be equal, does it depend on set ${\cal P}$ of predicates) |
- | * the precision of computed information, that is, the sets $\gamma(g_A(p))$ and $\gamma(g_B(p))$ for an arbitrary program point $p \in V$ | + | * the precision of computed information, that is, comparison of sets $\gamma(g_A(p))$ and $\gamma(g_B(p))$ for an arbitrary program point $p \in V$. |