Abstract Interpretation Assignment

Apa0506

%TOC%

---+++ In short

This assignment comprises a number of exercises of equal weight.

<p>
The general rule is: *Motivate your answers*
</p>

---+++ The assignment

The full assignment is available as a [[http://www.cs.uu.nl/docs/vakken/apa/apaabsint.pdf][PDF download]].

---+++ What, how and when to submit

Details can be found [[CourseAssignments][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.

-- Main.JurriaanHage - 07 Jun 2005

Master Course Automatic Program Analysis

Abstract Interpretation Assignment

Master Course
Automatic Program Analysis