[M.Sc. Laboratory] Synthesis of Ranking Functions for Lasso Programs
|Course type||Master Laboratory
|Credits||Depending on course type 6, 12 or 30|
In  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 Andreas Podelski, Andrey Rybalchenko: A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI 2004:239-251