{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:03Z","timestamp":1776333483831,"version":"3.51.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T00:00:00Z","timestamp":1427760000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a new method for the constraint-based synthesis of termination\narguments for linear loop programs based on linear ranking templates. Linear\nranking templates are parameterized, well-founded relations such that an\nassignment to the parameters gives rise to a ranking function. Our approach\ngeneralizes existing methods and enables us to use templates for many different\nranking functions with affine-linear components. We discuss templates for\nmultiphase, nested, piecewise, parallel, and lexicographic ranking functions.\nThese ranking templates can be combined to form more powerful templates.\nBecause these ranking templates require both strict and non-strict\ninequalities, we use Motzkin's transposition theorem instead of Farkas' lemma\nto transform the generated $\\exists\\forall$-constraint into an\n$\\exists$-constraint.<\/jats:p>","DOI":"10.2168\/lmcs-11(1:16)2015","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:33:27Z","timestamp":1431934407000},"source":"Crossref","is-referenced-by-count":27,"title":["Ranking Templates for Linear Loops"],"prefix":"10.46298","volume":"Volume 11, Issue 1","author":[{"given":"Jan","family":"Leike","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4252-3558","authenticated-orcid":false,"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2015,3,31]]},"reference":[{"key":"1093:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/797\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/797\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:19Z","timestamp":1681242979000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/797"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,31]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(1:16)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1503.00193","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1503.00193","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-030-32409-4_27","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,31]]},"article-number":"797"}}