[Varies] Synthesis of Ranking Functions

Course type	Bachelor-Project, Bachelor Thesis or Master Thesis
Instructors	Matthias Heizmann
Credits	Depending on course type 6, 12 or 30
Course Catalog

Which of the following procedures are terminating for every input? Why?

waldkirch(x) {
  while (x>=0) {
    x--;
  }
}





.

selestat(x) {
  while (x>=0) {
    x++;
  }
}





.

telAviv(x,y) {
  while (x>=0 && y>=0) {
    if(random) {
      x:=min(x,y)-1;
    }
    else {
      y:=min(x,y)-1;
    }
  }
}
.

strasbourg(x,y) {
  while (x>=0 && y>=0) {
    if(random) {
      x--;
      y:= random;
    }
    else {
      y--;
    }
  }
}

We can easily prove termination of the procedures waldkirch, telAviv and strassbourg by showing that the functions

are ranking functions for the while loop in the procedures.

But how can we synthesize these ranking functions?

In this project we give an answer to this question, by

stating templates for ranking functions like e.g. f(x,y)=a * x + b * y + c and compute the parameters a, b, c using our theorem prover SmtInterpol
implementing this approach in our program analysis framework ULTIMATE