4.3k citations · 7.2k across the 45 of their papers we have counts for
4 papers · 1 filter
Geometric Series as Nontermination Arguments for Linear Lasso Programs
Jan Leike, Matthias Heizmann
We present a new kind of nontermination argument for linear lasso programs, called geometric nontermination argument. A geometric nontermination argument is a finite representation…
Ranking Function Synthesis for Linear Lasso Programs
Jan Leike
The scope of this work is the constraint-based synthesis of termination arguments for the restricted class of programs called linear lasso programs. A termination argument consists…
Linear Ranking for Linear Lasso Programs
Matthias Heizmann, Jochen Hoenicke, Jan Leike +1
The general setting of this work is the constraint-based synthesis of termination arguments. We consider a restricted class of programs called lasso programs. The termination argum…
Ranking Templates for Linear Loops
Jan Leike, Matthias Heizmann
We present a new method for the constraint-based synthesis of termination arguments for linear loop programs based on linear ranking templates. Linear ranking templates are paramet…