Skip navigation
Skip navigation

Ranking templates for linear loops

Leike, Jan; Heizmann, Matthias


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...[Show more]

CollectionsANU Research Publications
Date published: 2015
Type: Journal article
Source: Logical Methods in Computer Science
DOI: 10.2168/LMCS-11(1:16)2015


File Description SizeFormat Image
01_Leike_Ranking_templates_for_linear_2015.pdf257.58 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator