[Varies] Synthesis of Ranking Functions
Course type | Bachelor-Project, Bachelor Thesis or Master Thesis |
---|---|
Instructors | Matthias Heizmann1 |
Credits | Depending on course type 6, 12 or 30 |
Course Catalog |
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
- 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