Jan Leike ; Matthias Heizmann - Ranking Templates for Linear Loops

lmcs:797 - Logical Methods in Computer Science, March 31, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:16)2015
Ranking Templates for Linear Loops

Authors: Jan Leike ; Matthias Heizmann ORCID-iD

    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 parameterized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. Our approach generalizes existing methods and enables us to use templates for many different ranking functions with affine-linear components. We discuss templates for multiphase, nested, piecewise, parallel, and lexicographic ranking functions. These ranking templates can be combined to form more powerful templates. 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 $\exists\forall$-constraint into an $\exists$-constraint.


    Volume: Volume 11, Issue 1
    Published on: March 31, 2015
    Accepted on: June 25, 2015
    Submitted on: November 12, 2014
    Keywords: Computer Science - Logic in Computer Science

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-030-32409-4_27
    • 10.1007/978-3-030-32409-4_27
    • 10.1007/978-3-030-32409-4_27
    Synthesizing Nested Ranking Functions for Loop Programs via SVM
    Li, Yi ; Sun, Xuechao ; Li, Yong ; Turrini, Andrea ; Zhang, Lijun ;

    16 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 533 times.
    This article's PDF has been downloaded 451 times.