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

Secondary volumes: Selected Papers of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014)

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

25 Documents citing this article

Nils Lommen;Jürgen Giesl, 2025, AProVE (KoAT + LoAT), Lecture notes in computer science, pp. 205-211, 10.1007/978-3-031-90660-2_13, https://doi.org/10.1007/978-3-031-90660-2_13.

Daniel Baier;Dirk Beyer;Po-Chun Chien;Marek Jankola;Matthias Kettl;et al., 2024, CPAchecker 2.3 with Strategy Selection, Lecture notes in computer science, pp. 359-364, 10.1007/978-3-031-57256-2_21, https://doi.org/10.1007/978-3-031-57256-2_21.

Daniel Baier;Dirk Beyer;Po-Chun Chien;Marie-Christine Jakobs;Marek Jankola;et al., 2024, Software Verification with CPAchecker 3.0: Tutorial and User Guide, Lecture notes in computer science, pp. 543-570, 10.1007/978-3-031-71177-0_30, https://doi.org/10.1007/978-3-031-71177-0_30.

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.

Marcel Hark;Florian Frohn;Jürgen Giesl, 2023, Termination of triangular polynomial loops, Formal Methods in System Design, 65, 1-3, pp. 70-132, 10.1007/s10703-023-00440-z, https://doi.org/10.1007/s10703-023-00440-z.

Zhonghan Wang;Bohua Zhan;Bohan Li;Shaowei Cai, 2023, Efficient Local Search for Nonlinear Real Arithmetic, Lecture notes in computer science, pp. 326-349, 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, 2022, Improving Automatic Complexity Analysis of Integer Programs, Lecture notes in computer science, pp. 193-228, 10.1007/978-3-031-08166-8_10.

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

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

Yi Li;Yi Li;Xie Li;Yong Li;Yong Li;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, 2021, Automatic Discovery of Fair Paths in Infinite-State Transition Systems, Lecture notes in computer science, pp. 32-47, 10.1007/978-3-030-88885-5_3.

Hiroshi Unno;Tachio Terauchi;Eric Koskinen, 2021, Constraint-Based Relational Verification, Lecture notes in computer science, pp. 742-766, 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, Electronic Proceedings in Theoretical Computer Science, 344, pp. 13-21, 10.4204/eptcs.344.2, https://doi.org/10.4204/eptcs.344.2.

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

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

Amir M. Ben-Amram;Jesús J. Doménech;Samir Genaim, 2019, Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets, arXiv (Cornell University), pp. 459-480, 10.1007/978-3-030-32304-2_22, http://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, 2019, Synthesizing Nested Ranking Functions for Loop Programs via SVM, Lecture notes in computer science, pp. 438-454, 10.1007/978-3-030-32409-4_27.

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

Jan Leike;Matthias Heizmann, 2018, Geometric Nontermination Arguments, arXiv (Cornell University), pp. 266-283, 10.1007/978-3-319-89963-3_16, http://arxiv.org/abs/1609.05207.

Yi Li;Tianxun Cai;Yong Feng, 2018, A Sufficient Criterion for Termination of Multi-path Linear Assignment Loops, Communications in computer and information science, pp. 223-237, 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, 2017, On Multiphase-Linear Ranking Functions, Lecture notes in computer science, pp. 601-620, 10.1007/978-3-319-63390-9_32.

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3667 times.

This article's PDF has been downloaded 1119 times.