2014/01/21 by Jan Leike, Leike, Jan, Matthias Heizmann +1 · 1 citation
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1401.5338
openalex publication_date 2014/01/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 parametrized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. This approach generalizes existing methods and enables us to use templates for many different ranking functions with affine-linear components. We discuss templates for multiphase, piecewise, and lexicographic ranking functions. Because these ranking templates require both strict and non-strict inequalities, we use Motzkin's Transposition Theorem instead of Farkas Lemma to transform the generated ∃∀-constraint into an ∃-constraint.