« January 2018 »
January
MoTuWeThFrSaSu
1234567
891011121314
15161718192021
22232425262728
293031
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