[M.Sc. Laboratory] Synthesis of Ranking Functions for Lasso Programs
Course type | Master Laboratory |
---|---|
Instructors | Matthias Heizmann |
Credits | Depending on course type 6, 12 or 30 |
Course Catalog |
In [1] a linear constraint solver is used to synthesize linear ranking functions for programs which consist of a single loop. In this project we extend this approach to lasso programs.
Literature
[1] Andreas Podelski, Andrey Rybalchenko: A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI 2004:239-251