Termination Analysis of Linear-Constraint Programs
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911398618988544 |
|---|---|
| author | Ben-Amram, Amir M. Genaim, Samir Ouaknine, Joël Worrell, James |
| author_facet | Ben-Amram, Amir M. Genaim, Samir Ouaknine, Joël Worrell, James |
| contents | This Survey provides an overview of techniques in termination analysis for programs with numerical variables and transitions defined by linear constraints. This subarea of program analysis is challenging due to the existence of undecidable problems, and this Survey systematically explores approaches that mitigate this inherent difficulty. These include foundational decidability results, the use of ranking functions, and disjunctive well-founded transition invariants. The Survey also discusses non-termination witnesses, used to prove that a program will not halt. We examine the algorithmic and complexity aspects of these methods, showing how different approaches offer a trade-off between expressive power and computational complexity. The Survey does not discuss how termination analysis is performed on real-world programming languages, nor does it consider more expressive abstract models that include non-linear arithmetic, probabilistic choice, or term rewriting systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_06752 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Termination Analysis of Linear-Constraint Programs Ben-Amram, Amir M. Genaim, Samir Ouaknine, Joël Worrell, James Programming Languages Logic in Computer Science This Survey provides an overview of techniques in termination analysis for programs with numerical variables and transitions defined by linear constraints. This subarea of program analysis is challenging due to the existence of undecidable problems, and this Survey systematically explores approaches that mitigate this inherent difficulty. These include foundational decidability results, the use of ranking functions, and disjunctive well-founded transition invariants. The Survey also discusses non-termination witnesses, used to prove that a program will not halt. We examine the algorithmic and complexity aspects of these methods, showing how different approaches offer a trade-off between expressive power and computational complexity. The Survey does not discuss how termination analysis is performed on real-world programming languages, nor does it consider more expressive abstract models that include non-linear arithmetic, probabilistic choice, or term rewriting systems. |
| title | Termination Analysis of Linear-Constraint Programs |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2509.06752 |