Model-Checking SS 2012

Exercise 1: April 18 (discussion on April 20)

1. Recap of logic. Read Tom Henzinger's "How To Write a Proof" and Sections 1.1 - 1.6 in this book (PDF).
2. Prove or give a counterexample: ((∀ y: P(y)) ∨ (∀ z: Q(z))) → (∀ x: P(x) ∨ Q(x)).
3. Prove or give a counterexample: (∀ x: P(x) ∨ Q(x)) → ((∀ y: P(y)) ∨ (∀ z: Q(z))).

Exercise 2: April 24 (discussion on April 27)

1. Prove the following equivalence:
   ∀ V ∀ V' : H(V) ∧ R(V, V') → H(V')
   if and only if
   for all s and for all s' holds if s ⊧ H(V) and (s, s') ⊧ R(V, V') then s' ⊧ H(V)


2. Prove that if a program is safe then there exists H(V) (in an expressive assertion language) such that
   ∀ V: φ_init(V) → H(V)
   ∀ V ∀ V' : H(V) ∧ R(V, V') → H(V')
   ∀ V: H(V) ∧ φ_error(V) → ⊥
3. Prove that if a program terminates then there exists H(V), a well-founded set (W, ≺), and a function r : States → W such that
   ∀ V: φ_init(V) → H(V)
   ∀ V ∀ V' : H(V) ∧ R(V, V') → H(V') ∧ r(V) ≻ r(V')

Exercise 3: May 2 (discussion on May 4)

1. Study the termination proof for the Basic Reachability Algorithm (BRA) (see PDF).
2. Prove that upon termination of BRA, if a node n is reachable from the initial node n₀ via the set of edges E, i.e., (n₀, n) ∈ E^*, then n ∈ C.
3. Extend the BRA algorithm to detect the existence of cycles in a given finite graph. The extended algorithm returns true iff there exists n ∈ N such that (n₀, n) ∈ E^* and (n, n) ∈ E⁺.

1. Study the definition and examples of the post operator, see PDF.
2. Give a program P that contains a single transition such that the reachability compuation using post diverges for P.

1. Install OCaml. On Linux: sudo apt-get install ocaml. On OSX with ports: sudo port install ocaml.
2. Install git. On Linux: sudo apt-get install git. On OSX with ports: sudo port install git.
3. Create a working directory:

   cd
   mkdir mc2012
   

4. Install CIL from github:

   cd mc2012
   git clone https://github.com/kerneis/cil.git
   cd cil
   ./configure
   make
   cd ..
   

   Execute pwd and remember the output string. You will need this string in Step 6.
5. Download the CFG bundle and save it in the directory mc2012, e.g., by executing wget http://archive.model.in.tum.de/um/courses/mc/ss2012/cfg.tgz Unpack the bundle using command tar xzf cfg.tgz. You should obtain a directory mc2012/cfg. Change the working directory to mc2012/cfg by executing cd cfg.
6. Edit config.make: i) uncommend a line with your OS, ii) adjust the variable CIL such that it is assigned the directory obtained by running pwd in Step 3.
7. Execute make
8. Execute

   src/main.native test/mytest.c > cfg.dot
   cat cfg.dot
   

9. Install a dot file viewer from Graphviz and use it to visualize the content of cfg.dot. Discover a correspondance between the control-flow graph in cfg.dot and the source code of test/mytest.c.

Exercise 4: May 9 (discussion on May 11)

1. Below we show a modified version of BRA together with a cycle detection algortihm, which uses BRA. Implement the presented cycle detection algorithm in Ocaml.

   algorithm BRA
          input
            N : set of nodes
            n0 : start node, where n0 \in N
            E : set of edges, where E \subseteq N \times N
         var
            C : nodes reached so far
            done : Boolean flag
            D : auxiliary set of nodes
          begin
            C := {n0}
            done := false
            while \neg done do
              D := { d \in N | \exists c \in C: (c, d) \in E }
              if \neg (D \subseteq C) then
                C := C \cup D
              else
                done := true
            od
   	 return (C, D)
   end
   
   algorthm detect_cycle
   input
            N : set of nodes
            n0 : start node, where n0 \in N
            E : set of edges, where E \subseteq N \times N
   
   begin
           (C, D) := BRA (N, N0, Edges)
           foreach s in C 
   		(Cs,Ds) := BRA (N, s, Edges)
   		if  (s \in Ds) then
   		    return true             
   	 return false
   end
   

2. Let R be a transition relation over V and V'. We define post(φ) = ∃ V" : φ[V"/V] ∧ R[V"/V][V/V']. Prove (∨ _{i>= 0} post ^{# i} (φ_init)) ⊧ (∨ _{j>= 0} post ^{# j} (α (φ_init))).
3. Prove:
   1. ∀ φ : φ ⊧ α (φ).
   2. α is monotonic, i.e., ∀ φ ∀ ψ : (φ ⊧ ψ) → (α (φ) ⊧ α (ψ)).
   3. ∀ φ ∀ R1 ∀ R2 : post(φ, R1 ∨ R2) iff ∀ φ ∀ R1 ∀ R2 : (post(φ, R1) ∨ post(φ, R2)).
4. Give an inductive invariant that proves safety for each of the following programs.

   1. main(int x, int y) {
        assume(x == 0);
        if(y >= 0)
          y++;
        else
          y=1;
        assert(y > x);
      }
      

   2. main(int n) {
        int i, j;
        assume(n >= 0);
        i = 0; j = n;
        while(i < j) { i++; j--; }
        assert(i+j == n);
      }
      

   3. main(int n) {
        int i; int j; bool inc; 
        i = 0; j = n; inc = false;
        while(i < n) {
          if(not inc) {
            j++; inc = true;
          } else {
            j--; inc = false;
          }
          i++;
        }
        assert(j =< n+1);
      }
      

5. Install SICStus prolog, and implement the "hello world" program and a binary search program for ordered lists. A good reference can be the SICStus prolog user manual. Some of the main prolog constructs that will be used in the course will be discussed in the tutorial.

Exercise 5: May 16 (discussion on May 18)

1. We define a constraint C₁ over ϕ₁, ϕ₂, and ϕ₃ as follows.
   
   C₁(ϕ₁, ϕ₂, ϕ₃) ≡
        ϕ _init ⊧ ϕ₁ ∧
        post(ϕ₁, ρ₁) ⊧ ϕ₂ ∧
        post(ϕ₂, ρ₂) ⊧ ϕ₃ ∧
        ϕ₃ ∧ ϕ_err ⊧ false
   
   Prove that for each ϕ₁, ϕ₂, and ϕ₃ if C₁(ϕ₁, ϕ₂, ϕ₃) then ϕ _init ∧ (ρ₁ o ρ₂) ∧ ϕ_err[V"/V] ⊧ false.
2. We define a constraint C₁ over ϕ₁ and ϕ₂ as follows.
   
   C₂(ϕ₁, ϕ₁) ≡
        ϕ _init ⊧ ϕ₁ ∧
        post(ϕ₁, ρ₁) ⊧ ϕ₂ ∧
        post(ϕ₂, ρ₂) ∧ ϕ_err ⊧ false
   
   Prove that C₁ is satisfiable if and only if C₂ is satisfiable, where C₁ is defined in the previous question.
3. Prove that post(post(ϕ, ρ₁), ρ₂) is equivalent to post(ϕ, ρ₁ o ρ₂)

Exercise 6: May 23 (discussion on May 25)

1. Compute interpolants for:
   1. x < 5, y ≤ x and y ≥ 10
   2. x < 5 and x ≥ y, y ≥ 10
   3. x+1 ≤ z and x ≥ y, y ≥ z
2. Prove that our interpolation algorithm respects the condition imposed on the variables that occur in the computed interpolant.
3. Prove that if Ax ≤ a ∧ Bx ≤ b ⊧ false then there exists ix ≤ i₀ that is an interpolant.
4. Represent inference rules describing summarization as entailments.
5. Compute summaries for the following program:

   
   f() {
     if (*) f();
   }
   main() {
     assume(*);
     f();
     assert(*);
   }
   

The prolog implementations of abstract and abstract_Reachability

Exercise 7: June 05 (discussion on June 08)

1. For the program producer-consumer with semaphores, prove the stability of the inductive invariant given in class under transitions PW→PM and CI→CL.
2. Consider the Dijkstra's two-threaded algorithm. Prove or refute that the inductive invariant given in class is the strongest one, i.e. that every invariant that implies the given one is already equivalent to the given one.
3. The following mutual exclusion algorithm for 2 threads is suggested:
   

   Initially turn∈{1,2}∧Q1=Q2=0.
   // Thread 1	// Thread 2
   while(true) { // noncritical section A: Q1:=true B: turn:=1 C: await ¬Q2 ∨ turn=2 // critical section D: Q1:=false // nocritical section }	while(true) { // noncritical section A: Q2:=true B: turn:=2 C: await ¬Q1 ∨ turn=1 // critical section D: Q2:=false // noncritical section }

   Prove or refute the mutual exclusion property, which here says that in any state reachable from the initial ones the two threads are not simultaneously at the critical locations D. You may assume that the threads start at locations A and the transitions between each pair of labels is atomic.

Exercise 8: June 12 (discussion on June 15)

1. In class a formula I for the Szymanski's mutual exclusion protocol was given.
   1. Prove that I is stable under each transition at locations l₅ till l₁₂ of each thread.
   2. Show that I implies the mutual exclusion property, namely, that ∀ i,j∈Tid: l_i=10=l_j⇒i=j.
   3. Assume that the transition at location l₁₁ is replaced by a no-operation (which changes just the program counter of the executing thread, while the remaining variables retain their values). Is the mutual exclusion property still satisfied?
2. (An optional task with an increased difficulty level.) Let (L, ≤) be a complete lattice (i.e. a partial order in which for every set A ⊆ L, the least upper bound sup A and the greatest lower bound inf A exist). Let f:L→L.
   1. If f is monotone, then the least fixpoint of f, written lfp(f), exists and is equal to inf {x∈L | f(x)=x} = inf {x∈L | f(x)≤x }.
   2. If for all nonempty chains C ⊆ L we have sup f(C) = f (sup C), then lfp(f) = sup {fⁱ(inf L)|i∈N₀}.

Exercise 9: June 20 (discussion on June 22)

1. Infer the type in the empty typing environment: let fun f x y = if x > y then true else false in f 0 end
2. Which typing environment is obtained by typing the following declarations in the empty typing environment:
   1. val t = 3
   2. fun fib n = if n < 3 then 1 else fib (n-1) + fib(n-2)
   3. fun square r = let fun exp y x = if y = 0 then 1 else if y < 0 then 0 else x * (exp (y-1) x) in exp 2 r end
3. Which sequence of value environments is obtained by evaluating the following program?
   

   fun f x = if x then 1 else 0;
   val x = 5*7;
   fun g z = f (z < x) < x;
   val x = g 5;
   val k = let fun h x = x * x in h end;
   

4. Evaluate the following expression:
   

   let
     fun square r = 
     let fun exp y x  = if y = 0 then 1 else if y < 0 then 0 else x * (exp (y-1) x)
     in
    exp 2 r
   end
   in
     square 5
   end
   

5. Formalize as a refinement type: the value of x is a negative integer that is greater then the sum of values of y and z.
6. Formalize as a refinement type: the value of f is a function that takes as input a positive integer and returns the doubled value.

Exercise 10: June 27 (discussion on June 29)

Exercise 11: July 2 (discussion on July 6)

(almost) All homework exercises with their suggested solutions

All mini-tests with their suggested solutions