« April 2018 »
April
MoTuWeThFrSaSu
1
2345678
9101112131415
16171819202122
23242526272829
30
Uni-Logo
You are here: Home Teaching Student Projects and Thesis Topics Finished [Varies] Synthesis of Ranking Functions
Document Actions

[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
Personal tools