Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

Ranking templates for linear loops

Simple item page
dc.contributor.authorLeike, Jan
dc.contributor.authorHeizmann, Matthias
dc.date.accessioned2015-12-13T22:16:27Z
dc.date.issued2015
dc.date.updated2015-12-11T07:26:18Z
dc.description.abstractWe 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 ∃∀-constraint into an ∃-constraint.
dc.identifier.issn1860-5974
dc.identifier.urihttp://hdl.handle.net/1885/70873
dc.publisherInternational Federation of Computational Logic (IfCoLog)
dc.sourceLogical Methods in Computer Science
dc.titleRanking templates for linear loops
dc.typeJournal article
local.bibliographicCitation.issue1
local.bibliographicCitation.lastpage27
local.bibliographicCitation.startpage16/1
local.contributor.affiliationLeike, Jan, College of Engineering and Computer Science, ANU
local.contributor.affiliationHeizmann, Matthias, University of Freiburg
local.contributor.authoruidLeike, Jan, u5485774
local.description.embargo2037-12-31
local.description.notesImported from ARIES
local.identifier.absfor080401 - Coding and Information Theory
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
local.identifier.ariespublicationa383154xPUB2451
local.identifier.citationvolume11
local.identifier.doi10.2168/LMCS-11(1:16)2015
local.identifier.scopusID2-s2.0-84927655213
local.type.statusPublished Version

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
01_Leike_Ranking_templates_for_linear_2015.pdf
Size:
257.58 KB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS

abcd