Ranking Templates for Linear Loops

Jan Leike; Matthias Heizmann

doi:10.2168/LMCS-11(1:16)2015

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 LoopsArticle

Authors: Jan Leike ; Matthias Heizmann

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.

https://doi.org/10.2168/LMCS-11(1:16)2015

Source: arXiv.org:1503.00193

Volume: Volume 11, Issue 1

Published on: March 31, 2015

Imported on: November 12, 2014

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Sources:

[1] zbMATH Open.

Bibliographic References

21 Documents citing this article

Jianan Yao;Runzhou Tao;Ronghui Gu;Jason Nieh, 2024, Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions, Proceedings of the ACM on Programming Languages, 8, POPL, pp. 1028-1059, 10.1145/3632877, https://doi.org/10.1145/3632877.

Zhonghan Wang;Bohua Zhan;Bohan Li;Shaowei Cai, Lecture notes in computer science, Efficient Local Search for Nonlinear Real Arithmetic, pp. 326-349, 2023, 10.1007/978-3-031-50524-9_15.

Alessandro Cimatti;Alberto Griggio;Enrico Magnago, 2022, LTL falsification in infinite-state systems, Information and Computation, 289, pp. 104977, 10.1016/j.ic.2022.104977.

Jürgen Giesl;Nils Lommen;Marcel Hark;Fabian Meyer, arXiv (Cornell University), Improving Automatic Complexity Analysis of Integer Programs, pp. 193-228, 2022, 10.1007/978-3-031-08166-8_10, https://arxiv.org/abs/2202.01769.

Mirco Giacobbe;Daniel Kroening;Julian Parsert, arXiv (Cornell University), Neural termination analysis, 24, pp. 633-645, 2022, Singapore Singapore, 10.1145/3540250.3549120, https://arxiv.org/abs/2102.03824.

Nils Lommen;Fabian Meyer;Jürgen Giesl, Lecture notes in computer science, Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops, pp. 734-754, 2022, 10.1007/978-3-031-10769-6_43, https://doi.org/10.1007/978-3-031-10769-6_43.

Yi Li;Xie Li;Yong Li;Xuechao Sun;Andrea Turrini;et al., 2022, Synthesizing ranking functions for loop programs via SVM, Theoretical Computer Science, 935, pp. 1-20, 10.1016/j.tcs.2022.07.002.

Alessandro Cimatti;Alberto Griggio;Enrico Magnago, Lecture notes in computer science, Automatic Discovery of Fair Paths in Infinite-State Transition Systems, pp. 32-47, 2021, 10.1007/978-3-030-88885-5_3.

Hiroshi Unno;Tachio Terauchi;Eric Koskinen, Lecture notes in computer science, Constraint-Based Relational Verification, pp. 742-766, 2021, 10.1007/978-3-030-81685-8_35, https://doi.org/10.1007/978-3-030-81685-8_35.

Jesús J. Domenech;Samir Genaim, 2021, Termination Analysis of Programs with Multiphase Control-Flow, arXiv (Cornell University), 344, pp. 13-21, 10.4204/eptcs.344.2.

Florian Frohn;Marcel Hark;Jürgen Giesl, Lecture notes in computer science, Termination of Polynomial Loops, pp. 89-112, 2020, 10.1007/978-3-030-65474-0_5.

Xie Li;Yi Li;Yong Li;Xuechao Sun;Andrea Turrini;et al., Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, SVMRanker: a general termination analysis framework of loop programs via SVM, pp. 1635-1639, 2020, Virtual Event USA, 10.1145/3368089.3417930.

Amir M. Ben-Amram;Jesús J. Doménech;Samir Genaim, arXiv (Cornell University), Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets, pp. 459-480, 2019, 10.1007/978-3-030-32304-2_22, https://arxiv.org/abs/1811.07340.

Yi Li;Wenyuan Wu;Yong Feng, 2019, On ranking functions for single-path linear-constraint loops, International Journal on Software Tools for Technology Transfer, 22, 6, pp. 655-666, 10.1007/s10009-019-00549-9.

Yi Li;Xuechao Sun;Yong Li;Andrea Turrini;Lijun Zhang, Lecture notes in computer science, Synthesizing Nested Ranking Functions for Loop Programs via SVM, pp. 438-454, 2019, 10.1007/978-3-030-32409-4_27, https://doi.org/10.1007/978-3-030-32409-4_27.

Yong Li;Andrea Turrini;Yu-Fang Chen;Lijun Zhang, Lecture notes in computer science, Learning Büchi Automata and Its Applications, pp. 38-98, 2019, 10.1007/978-3-030-17601-3_2.

Jan Leike;Matthias Heizmann, Lecture notes in computer science, Geometric Nontermination Arguments, pp. 266-283, 2018, 10.1007/978-3-319-89963-3_16, https://doi.org/10.1007/978-3-319-89963-3_16.

Yi Li;Tianxun Cai;Yong Feng, Communications in computer and information science, A Sufficient Criterion for Termination of Multi-path Linear Assignment Loops, pp. 223-237, 2018, 10.1007/978-981-13-1026-3_17.

Yu-Fang Chen;Matthias Heizmann;Ondřej Lengál;Yong Li;Ming-Hsien Tsai;et al., 2018, Advanced automata-based algorithms for program termination checking, ACM SIGPLAN Notices, 53, 4, pp. 135-150, 10.1145/3296979.3192405.

Amir M. Ben-Amram;Samir Genaim, arXiv (Cornell University), On Multiphase-Linear Ranking Functions, pp. 601-620, 2017, 10.1007/978-3-319-63390-9_32, https://arxiv.org/abs/1703.07547.

Matthias Heizmann;Daniel Dietsch;Marius Greitschus;Jan Leike;Betim Musa;et al., Lecture notes in computer science, Ultimate Automizer with Two-track Proofs, pp. 950-953, 2016, 10.1007/978-3-662-49674-9_68.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1979 times.

This article's PDF has been downloaded 798 times.