Home Exam

    Section 1: Small Questions (60%)

  1. Give an example of a partially ordered set which is not a lattice
  2. Give an example of a function on a lattice which is not monotone and not anti-monotone (A function f is anti-monotone

    3. if for every x1, x2, such that x1 <= x2, f(x2) <= f(x1))
  3. Give an example of a Galois connection which is not a Galois insertion
  4. Given an example which shows that the widening operator in the interval lattice is not monotone in both of its arguments (A function f:D*D->D is monotone in both arguments if for every d1, d2, d3 such that d1<=d2, f(d1, d3)<=f(d2, d3) and

    5. f(d3, d1)<=f(d3, d2)).
  5. What does the above example imply on the interval analysis which uses widening?
  6. Give an object oriented program (in Java or C++) with a virtual function which is only invoked once in which the control flow analysis given in class will fail to detect that.

    7.  

    Section 2: TVLA(40%)


    Solve one of the following projects

    Project 1: Proving Partial Correctness of a Simple Mark and Sweep Garbage Collection

    1. Document the predicates and the actions in the tvp files for the Mark and Sweep example. In particular, explain the instrumentation predicates and their meanings (15%).
    2. Remove the focus operations in stat_set.tvp and study the resulting analysis (15%)
    3. What are the difficulties in extending the analysis to handle Garbage Collection Algorithms like Copy Garbage Collection in which the garbage collector can mutate the heap (10%)

      4. (Bonus) Add actions for showing that the Mark phase musty eventually terminate. One way to show that is by showing that on every loop iteration in the set of nodes reachable from the pointer variable x used in the while loop condition (in mark.tvp) (15%)

Project 2: Proving Partial Correctness of Sorting Algorithm

  1. Document the predicates and the actions in the tvp files for the sorting example. In particular, explain the instrumentation predicates and their meanings (5%).
  2. Remove the focus operations in cond.tvp and study the resulting analysis (10%)
  3. Write an improved version of bubble sort in C called smart-bubble-sort which stops once the list is sorted and doesn't compare elements which are already in place (using linked lists and pointers). Then, convert it manually into tvp and run it. Study the results of the analysis (25%)
  4. (Bonus) Add actions for showing that the loops in insertion sort and bubble sort must eventually terminate. One way to show that is by showing that on every loop iteration in the set of nodes reachable from the temporary variable x  (15%)

 
 
 
 
 
 

Section 3: Only for students which did not prepare course notes (can be submitted srperately by July 28th)

   Design an algorithm for points-to analysis in PWhile which uses set constraints.
  1.   Show how sets constraints are generated in a syntax directed matter for PWhile
  2.   Compare the precision of the solution with the one developed in class using Chaotic Iterations (April 25 class)
  3.   Construct the set of constraints in the above example and apply the graph based cubic iterative algorithm to find the minimal solution for the the set of constraints in the example PWhile program
x := 2
y1 := &x
y2 := &y1
y3 := &y2
while x >0 (
        y3 := *y3
        x := x -1
)
*y3 := 7
z := x
     

    Good Luck!!!