4.3k citations · 7.2k across the 45 of their papers we have counts for
7 papers · 1 filter
Geometric Nontermination Arguments
Jan Leike, Matthias Heizmann
We present a new kind of nontermination argument, called geometric nontermination argument. The geometric nontermination argument is a finite representation of an infinite executio…
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…
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…