You are here: Home Student Projects and … Finished [Varies] Synthesis of Ranking …

[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?

 

  We can easily prove termination of the procedures waldkirch, telAviv and strassbourg by showing that the functions
  • f: ℤ -> ,  f(x)=x
  • f: ℤxℤ -> ℕ ,  f(x,y)=min(x,y)
  • f: ℤx -> ℕxℕ ,  f(x,y)=(x,y)

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