Ranking Templates for Linear Loops

DOI10.2168/LMCS-11(1:16)2015zbMath1391.68020arXiv1503.00193OpenAlexW1525126490MaRDI QIDQ5246721

Jan Leike, Matthias Heizmann

Publication date: 22 April 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1503.00193

zbMATH Keywords

terminationFarkas' lemmaMotzkin's theoremnested ranking functionlinear loop programwell-founded relationlexicographic ranking functionlinear lasso programlinear ranking templatemultiphase ranking functionparallel ranking functionpiecewise ranking function

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Constraint-based relational verification ⋮ Reflections on termination of linear loops ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Termination of polynomial loops ⋮ Proving Termination Through Conditional Termination ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ Automatic complexity analysis of integer programs via triangular weakly non-linear loops ⋮ \textsc{LTL} falsification in infinite-state systems

This page was built for publication: Ranking Templates for Linear Loops