39 citations · 66 across the 9 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…
Termination Analysis by Learning Terminating Programs
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trac…
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…