Predicates and Prejudice - Proving Correctness of Programs

Predicates

In which of the following procedures does the assert statement never fail? Why?

procedure raven(int x, int y, int z)
{
  y := x;

  while (random()) {
    x := x + 1;
    y := y + 1;
  }

  assert(x==z ==> y==z);
}

procedure blackbird(int x, int y)
{
  x := 0;
  y := x;

  while (random()) {
    x := x + 1;
  }

  assert(x != -1 && y != -1);
}

• We can prove that the assertion in the procedure raven never fails by showing that the predicate y==x is a loop invariant of the while loop.
• We can prove that the assertion in the procedure blackbird never fails by showing that the predicates x>=0 and y==0 are loop invariants of the while loop.

Given these predicates, the correctness of the procedures can easily be shown using a technique called predicate abstraction. The question is: how do we guess the right predicates?

Prejudice

• It is said that every German loves football. However this is not true, I know some Germans that don't like football at all. But if you meet some German the chance is high that he or she likes football.
• It is said that it is always raining in Scotland. However this is not true. But there are regions in Scotland where the risk of rain is much higher than in Freiburg.

Predicates and Prejudice

• If a procedure contains the statement y:=x then the predicate y==x is useful in a correctness proof. Of course this is not always true, the procedure blackbird is a counterexample. But for some procedures the predicate y==x is a good guess.
• If a procedure contains the statement x:=0 and the statement x:=x+1 then the predicate x>=0 is useful in a correctness proof. Of course this is not always true, the procedure raven is a counterexample. But for some procedures the predicate x>=0 is a good guess.

Tasks

1. We will implement the predicate abstraction technique in our software model checker ultimate.
2. We will develop methods to extract useful predicates from the program.
3. We will realize that if we use all extracted predicates our tool will run out of memory.
4. We will state "prejudices" about usefulness of  a predicates.
   
5. We will evaluate the significance of our prejudice using machine learning techniques.
   

 The number of tasks done in the project depends on the course type.