WebHome
- Education Page
- Description
- Literature
- Schedule
- Assignments
- Software

Center
Master Program

Center

Page

Web

Wiki

# Abstract Interpretation Assignment

Apa0506

### In short

This assignment comprises a number of exercises of equal weight.

### What, how and when to submit

Details can be found here. In whatever fashion you hand things in make sure things are clear and readable and on time.

### Experiences from last year

For some of these exercises it is handy to reuse some of the Galois Insertions I defined in the slides. You may reuse these at will, and do not have to prove their correctness.

Exercise 4.11 seems a bit unclear with all the indices/variables called n. The way to read the definition of Y (capital upsilon) is that if you are given two ascending chains x and y, that are equal for the first Y(x) elements, then Y(x) = Y(y).

In Mini Project 4.1 it is not clear what should be the ordering on lists. A natural choice is x \subseteq y if and only if x is a prefix of y. However, you do not really need this ordering, since you only have to complete the specification, not give a proof that it is a Galois Connection/Insertion. Still, a few examples to convince yourself that you are not too far off the mark can be helpful.

-- JurriaanHage - 07 Jun 2005