## Problem 1

Galois connection is defined by two monotonic functions and between partial orders on and on , such that

for all and (intuitively, the condition means that is approximated by ).

**Part a)** Show that the condition is equivalent to the conjunction of these two conditions:

hold for all and .

**Part b)** Let and satisfy the condition of Galois connection. Show that the following three conditions are equivalent:

- for all
- is a surjective function
- is an injective function

**Part c)** State the condition for to hold for all . When is the set of sets of concrete states and is a domain of static analysis, is it more reasonable to expect that or to be satisfied, and why?

## Problem 2

Suppose you are given a set of predicates in a decidable theory of first-order logic (for example, quantifier-free formulas in the combination of uninterpreted function symbols with integer linear arithmetic) where 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 b)** Describe how to construct from a new, smaller, lattice , where the above equivalence holds. Is there an algorithm to compute and the partial order on using a decision procedure for the logic of predicates?

**Part c)** Suppose that, for the same set of predicates, we use lattice and lattice to compute the fixpoints and of the function from Abstract Interpretation Recipe. What can you say about

- the comparison of numbers of iterations needed to compute the fixpoint and (is one always less than the other, can they be equal, does it depend on set of predicates)
- the precision of computed information, that is, comparison of sets and for an arbitrary program point .