39 citations · 66 across the 9 of their papers we have counts for
8 papers · 1 filter
Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
Laurent Fribourg, Matthias Heizmann
The proceedings consist of a keynote paper by Alberto followed by 6 invited papers written by Lorenzo Clemente (U. Warsaw), Alain Finkel (U. Paris-Saclay), John Gallagher (Roskilde…
Ultimate TreeAutomizer (CHC-COMP Tool Description)
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke +2
We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attracti…
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…
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…