Model-Checking SS 2013

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

Exercises 1: April 26 (discussion on April 26)

1. Recap of logic. Read Tom Henzinger's "How To Write a Proof".
2. Prove or give a counterexample: (∀ x: ∀ y: p(x,y) → q(x)) → (∀ x: (∃ y: p(x,y)) → q(x)).
3. Does the linear arithmetic satisfaction relation (M |=LI phi) hold for
   M = {v1 |-> -2, v2 |-> 3} and
   phi = (2v1-3v2<=5) ?
4. Does the Horn clause satisfaction relation (M |=CL clauses) hold for
   M = { p(i) |-> (i>=-10) } and
   clauses = { i>=0 -> p(i), p(i) /\ i'=i+1 -> p(i') } ?
5. Run an inference algorithm for the set of clauses from the previous question.
   clauses = { i>=0 -> p(i), p(i) /\ i'=i+1 -> p(i') }
   Does the unbounded unfoldings algorithm terminate for this input? If yes, how does the solution obtained compare to the assignment M from the previous point?

Exercises 2: May 3 (discussion on May 3 to be continued on May 10)

1. Run the abstract inference algorithm to obtain a safety argument for the transition system given by
   init(V) = (pc=1 /\ s=0 /\ i=n)
   rho_r(V,V') = (pc=1 /\ pc'=1 /\ i>=0 /\ s'=s+i /\ i'=i-1 /\ n'=n) \/
   (pc=1 /\ pc'=2 /\ i<0 /\ s'=s /\ i'=i /\ n'=n)
   error(V) = (pc=2 /\ s<n)
2. Write down a termination argument for the program given in the previous exercise.
3. Write down, if possible, a termination argument for the transition system given by
   init(V) = true
   next(V,Vp) = (x<y /\ x'=x+1 /\ y'=y) \/ (x>=y /\ x'=x /\ y'=y)
   If you cannot find a termination argument, can you suggest how to modify the transition system so that all its computations become finite?

Homework 1: May 3 (deadline on May 10, submit by email to popeea at model.in.tum.de or on paper to my office 03.11.059)

1. Run the abstract inference algorithm for the program discussed at the tutorial on May 3, with the set of predicates Preds1 = {pc=1, s=0}. Can you conclude that the program is safe from the results of the abstract inference algorithm?
   The program is given below:
   init(V) = (pc=1 /\ s=0 /\ i=n)
   rho_r(V,V') = (pc=1 /\ pc'=1 /\ i>=0 /\ s'=s+i /\ i'=i-1 /\ n'=n) \/
   (pc=1 /\ pc'=2 /\ i<0 /\ s'=s /\ i'=i /\ n'=n)
   error(V) = (pc=2 /\ s<n)
2. Run the abstract inference algorithm for the same program, with the set of predicates Preds1 = {n<=s+i, pc=1, n<=s}. Can you conclude that the program is safe from the results of the abstract inference algorithm?

Exercises 3: May 10

1. Write down a termination argument for the following program:
   init(V) = (pc=1 /\ s=0 /\ i=n)
   rho_r(V,V') = (pc=1 /\ pc'=1 /\ i>=0 /\ s'=s+i /\ i'=i-1 /\ n'=n) \/
   (pc=1 /\ pc'=2 /\ i<0 /\ s'=s /\ i'=i /\ n'=n)
   
2. Write down, if possible, a termination argument for the transition system given by
   init(V) = true
   next(V,Vp) = (x<y /\ x'=x+1 /\ y'=y) \/ (x>=y /\ x'=x /\ y'=y)
   If you cannot find a termination argument, can you suggest how to modify the transition system so that all its computations become finite?
3. Write a computation that starts from the state s1=((ret |-> 0, n |-> 1, pc_main |-> l1), empty-stack) for the program:
   

   int ret;
   f(int i) {
     if (i>0) {
       f(i-1);
       ret = ret+i;
     } else {
     ret = 0;
     }
   }
   
   void main() {
     int n;
     f(n);
     assert(ret>=0);
     ret = ret;
   }
       

Exercises 4: May 16 (discussion on May 17)

1. Prove:
   1. ∀ φ, V: φ(V) → α (φ(V)).
   2. α is monotonic, i.e., ∀ φ, ψ: (∀V: φ(V) → ψ(V)) → (∀V: α (φ(V)) → α (ψ(V))).
2. Give an inductive invariant that proves safety for each of the following programs.

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

   2.    main(int n) {
           int i, j;
      l1:  assume(n >= 0);
      l2:  i = 0; j = n;
      l3:  while(i < j) { i++; j--; }
      l4:  assert(i+j == n);
      l5:}
      

   3.    main(int n) {
           int i; int j; bool inc; 
      l1:  i = 0; j = n; inc = false;
      l2:  while(i < n) {
      l3:    if(not inc) {
               j++; inc = true;
             } else {
               j--; inc = false;
             }
      l4:    i++;
           }
      l5:  assert(j <= n+1);
      l6:}
      

Exercises 5: May 23 (discussion on May 24)

1. Compute summaries for the following program:

       f() {
   m1:   if (*) 
   m2:     f();
   m3: }
   
       main() {
   l1:   assume(*);
   l2:   f();
   l3:   assert(*);
   l4: }
   

Homework 2: May 24 (deadline on May 30, noon; submit by email to popeea at model.in.tum.de or on paper to Corneliu)

1. Compute summaries for the procedures f and main using the unbounded inference algorithm.

       f() {
   m1:   if (*) 
   m2:     f();
   m3: }
   
       main() {
   l1:   assume(*);
   l2:   f();
   l3:   assert(*);
   l4: }
   

Exercises 6: May 24 (discussion on May 31)

1. Represent the entailments defining reachable states for multi-threaded programs as Horn clauses. Note that these entailments where given in the lecture from 13.05, pic4.
2. Use the unbounded inference algorithm to solve the Horn clauses obtained in the previous exercise with the following program:
   
      P = (N, VG, V1, V2, init, next1, next2)
      N = 2
      VG = (x)
      V1 = (pc1)
      V2 = (pc2)
      init(VG,V1) = (x=0 /\ pc1=A /\ pc2=C)
      next1(VG,V1,VG',V1') = (x'=x+1 /\ pc1=A /\ pc1'=B)
      next2(VG,V2,VG',V2') = (x'=x+2 /\ pc2=C /\ pc2'=D)
   
   Note that this transition system representation corresponds to a program with two threads and one global variable x initially 0.

   A: x=x+1;     ||     C: x=x+2;
   B:                   D:
   

   How many distinct concrete program states correspond to the solution you obtained? Note that a concrete program state is a triple with values for the variables x, pc1 and pc2.

Exercises 7: Jun 21 (discussion on demand on Jun 24, send email before Jun 24 to ruslan@model.in.tum.de)

Download the exercise sheet here.

Exercises 8: Jun 25 (discussion on Jun 28)

1. Let AP = {green, yellow, red} and σ = ({green}{green}{green}{yellow}{red}{red}{red}{yellow,red})^ω. Does σ satisfy the following properties:
   1. Xgreen ∨ yellow ,
   2. ¬greenUred ,
   3. ¬(greenUred) ?
2. Let AP = {green, yellow, red}. Write the following properties as LTL formulas (derived operators are allowed):
   1. Red and yellow occur together infinitely often.
   2. From some time point onward red and green never occur together.
   3. Whenever green turns on, green continues for at least two consecutive time units.
3. Consider a program P with States={s₀, s₁, s₂}, init={s₀}, transitions s₁→s₀→s₂→s₁. Let AP={a,b}. Let a label just s₁ and b label just s₂. Which of the following formulas hold for P?
   1. Fa ∧ Fb ,
   2. F(a∧b) ,
   3. Fa U G¬(a∧b) ,
   4. GFb .