Model-Checking SS 2010

News | Basic information | Content | Exercises | Slides | Links

Submit your solution by e-mail (put MC2010 in the subject line) and as a printout (don't forget to put your name).

In case of joint work, submit a single copy with names of all contributors.

Exercise 1: April 20

Due date: April 27, 9:55am CET.

Concrete enumerative reachability:

1. Prove that the algorithm in Fig. 2 is sound, i.e., computes all reachable states, and is complete, i.e., computes only reachable states.
2. Study the notion of path that is defined in Sec. 1.1. Extend the algorithm in Fig. 2 with the construction of counterexamples. That is, if a distinguished error location l_E is reachable then the algorithm returns a path that witnesses its reachability. Argue that the computed path serves as a counterexample.
3. Modify the algorithm in Fig. 2 such that it uses Pre instead of Post.
4. Modify the algorithm in Fig. 2 such that it uses WP instead of Post.

Exercise 2: April 20

Due date: April 27, 9:55am CET.

1. Download and build KLEE.
2. A protocol of building KLEE on Mac OS X. TXT
3. Go through tutorial one (testing a small function).
4. Provide a brief evaluation of your experience.

Exercise 3: May 4

Due date: May 1118, 9:55am CET.

1. Read Section 4.3.
2. Prove that the abstraction function Abs is at least as precise as the abstraction function CartAbs for a fixed set of predicates.
3. Let p1 /\ ... /\ pN = CartAbs(S, Preds) and q1 /\... /\ qM = CartAbs(T, Preds).
   Prove that CartAbs(S, Preds) implies CardAbs(T, Preds) if and only if {q1, ..., qM} is a subset of {p1, ..., pN}, or give a counterexample.
4. Download the ARMC model checker and its C frontend. LINK
   Write a small C procedure that includes a label ERROR and analyse its reachability using ARMC.
   Protocol your experience, esp. encountered limitations of the tool.
5. Install OCaml and study Chapter 1 (exclude Section 1.8 (Parsing)) of the OCaml manual.
6. Write an OCaml function print_all_bit_strings : n:int -> unit that prints all bit-strings of a given length n.
   Use the defintion of Abs from Section 4.3 as inspiration.
7. Given two disjoint rational convex hulls (i.e., systems of linear inequalities), prove that there exist a separating hyperplane (i.e., an inequality).
8. Prove that the interpolation for convex hulls presented in class and by the additional material PDF computes inequalities that are expressed over the shared variables of the input sets of inequalities.

Exercise 4: May 20

Due date: June 7, 9:55am CET.

1. Prove or disprove that &forall x : (∃ y: ψ(y) ∧ ρ(y, y'))[x/y'] → &psi(x) if and only if &forall x &forall x' : (ψ(x) ∧ ρ(x, x')) → &psi(x').
2. Apply the abstract reachability algorithm based on Cartesian abstraction function and the interpolation-based refinement procedure to prove for the program P1 below that the value of x at the location L is always non-negative. Present the computed abstract reachability trees, counterexample paths, their spuriousness analysis, and interpolant computation results.

   main() {
     int x;
     x = 0;
     L: x++;
     goto L;
   }
   

3. Apply the above algorithm on the program P2 below.

   main(int x, int y, int z) {
     assume(y >= z);
     while (x < y) {
       x++;
     }
     assert(x >= z);
   }
   

Exercise 5 (mid term test): June 10

1. Given a program P = (V, L, linit, lerror, {(li, reli, l{i+1})}), present an algorithm for the concerete enumerative safety verification.

2. Present Farkas' lemma and an example of its application.

3. Present a constraint-based algorithm for the interpolant computation 
   for a given pair of mutually disjoint convex rational hulls Ax \leq a and Bx \leq b.

4. Present a definition of Cartesian predicate abstraction and an example of its application.

5. Given the program

main() {
  rational x, y;
  if (x >= y && y >= 1 ) {
    assert(x >= 0);
  } 
}

5.1 Transform the program into a control-flow graph.
5.2 Present a counterexample to the assertion validity or prove the program correct 
    using Cartesian predicate abstraction and interpolation-based refinement (initially the set of predicates is empty). 
5.3 If the program is correct, present a safe inductive invariant.

6. Compute a ranking function for the loop

while (x <= y) {
  x++;
  y=y-2;
}

Present the constraint system used for the ranking function computation.

7. Proof or give a counterexample:
  (\forall x: (((\exists y: p(y) /\ q(y, y'))[x/y']) -> r(x))) if and only if (\forall x \forall x': ((p(x) /\ q(x, x')) -> r(x'))) 

Execise 6: June 15

Due date: June 21, 9:55am CET.

1. Extend the construction of the transition relation for programs with procedures with the treatment of nodes labeled START(_).
2. Extend the summarization-based concrete enumerative reachability algorithm with a rule/rules to deal with nodes labeled START(_).
3. Apply the summarization based algorithm on the program

   bool g = 1;
   main(bool a) {
   
     test(g || a);
   
   }
   
   test(bool x) {
     if (NONDET_CHOICE) {
       g = x;  
     } else {
       test(!g);  
     }
   }
   

   Present the reachable valuations of globals and locals, and the computed summaries.
4. Given a multi-threaded program and its transition relation T ⊆ TId x (G x L) x (G x L), compute a corresponding thread identifier-free transition relation Q ⊆ (G x L) x (sG x L) such that the reachability computation using T yields the same set of states as the reachability computation using Q.
5. Read Sections 1-2 in the paper Thread-Modular Model Checking. What is the main limitation of the thread-modular approach (see Section 1.2)?
6. Apply the thread-modular reachability computation on the program

   global bool lock = 0;
   Thread 1:
   
   A: get_lock(lock, 1);
   B:
   
   Thread 2:
   A: get_lock(lock, 1);
   B:
   

   where the function call get_lock(lock, 1); has the transition relation lock = 0 ∧ lock' = 1 together with the treatement of the program counter variable. Note that both threads write 1 into the lock variables. Present the rely and guarantee sets for each thread. Check if the computed rely sets imply the validity of the mutually exclusive access to the location B.

Execise 7: June 28

Due date: July 5, 9:55am CET.

1. Translate three properties from the list Things to avoid to LTL.
2. Prove the equivalences 1, 6, and 7 (counting from above) on Slide 13, and 6 on Slide 14. (slides)
3. 1. Translate the LTL formula G(req -> F ack) to a generalized Büchi automaton.
   2. Translate the obtained generalized Büchi automaton to a Büchi automaton.

Execise 8: July 13

Due date: July 20, 9:55am CET.
Exercise sheet.