# Ranking Templates for Linear Loops

arXiv: https://arxiv.org/abs/1401.5338 · HTML: https://mlsanity.com/paper/1401.5338/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Jan 2014.

## Built on by (most cited first, 2 of 2)

- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)

## Abstract (arXiv)

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 parametrized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. This approach generalizes existing methods and enables us to use templates for many different ranking functions with affine-linear components. We discuss templates for multiphase, piecewise, and lexicographic ranking functions. 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 existsforall-constraint into an exists-constraint.