# Termination analysis

Termination analysis proves that a program (or a particular loop or
recursion) always **halts**, rather than running forever. Termination is
a **liveness** property (*something good eventually happens*) rather than
a **safety** property (*nothing bad happens*).
Because termination is undecidable in general (the halting
problem), the analysis is **sound but incomplete**: a proof it produces
is correct, but for any tool there are terminating programs it cannot
certify.

The core idea is a **ranking function**, a measure that maps each
program state into a well-founded domain (often the naturals) and
*strictly decreases* on every iteration. Since a well-founded domain
has no infinite descending chain, a decreasing measure means the loop
cannot run forever. Modern tools synthesize these automatically
(Cook et al. 2011)[^cook2011].

## What it catches

- **Non-terminating loops and recursion.** Infinite loops, unbounded
  recursion, and algorithmic livelock: proven absent, not merely
  unobserved in testing.
- **Loss of progress in reactive code.** A control loop or protocol
  handler that can get stuck.

What it does **not** establish: anything about *what* the program
computes, only that it finishes. And by incompleteness, a "cannot
prove termination" result is not a proof of non-termination; it may
just be beyond the tool's ranking-function search.

## How it works

A single linear ranking function suffices for simple loops, but real
code needs more. The advance that made termination provable for
systems code was **transition invariants** and *disjunctive*
well-foundedness: proving termination by showing the transitive closure
of the program's transition relation is contained in a finite union of
well-founded relations, which reduces a liveness question to a **safety** check an
[abstract interpreter](https://quality.stereobooster.com/abstract-interpretation.md) can discharge
(Cook et al. 2011)[^cook2011]. A separate lineage, term-rewriting with dependency pairs,
underlies tools like AProVE. So termination analysis is not a single
technique but a family of ranking-argument syntheses.

## Tools and adjacent forms

- **[AProVE](https://aprove.informatik.rwth-aachen.de/)** — term-rewriting
  and dependency-pair termination for Java, C, Haskell, Prolog.
- **[Ultimate](https://ultimate-pa.org/)** — its Büchi Automizer
  proves termination (and non-termination) for C via automata.

Termination is also handled outside dedicated analyzers: total
languages such as [Agda](https://github.com/agda/agda) enforce it **by construction** with a
totality checker (see [types](https://quality.stereobooster.com/refinement-and-dependent-types.md)),
and static provers discharge it from a hand-written `decreases` /
`variant` metric (see [theorem proving](https://quality.stereobooster.com/theorem-proving.md) and
[contracts as specifications](https://quality.stereobooster.com/contracts-as-specifications.md)). Automated termination
analysis is the variant that *infers* the ranking argument instead of
requiring the author to supply it.

## When to use, when not

**Use** it where non-termination is a genuine failure mode: hard
real-time and reactive systems that must guarantee a response, OS and
driver loops, smart contracts (an unbounded loop is a denial-of-service
or out-of-gas failure), and total functional programming where
totality is part of the contract.

**Don't** reach for it for ordinary application code, where a hung
request is caught operationally by timeouts and
[monitoring](https://quality.stereobooster.com/monitoring-and-observability.md) at far lower
cost than a proof.

## Evidence

- **Scaling to systems code.** Termination tools can automatically prove
  or disprove termination of moderately sized industrial examples such as
  Windows device drivers (Cook et al. 2011)[^cook2011].

## Related

**Bounding a program's cost**

All three ask how much a computation costs, and meet the same undecidable core (the
halting problem) at different guarantee levels. Termination
analysis proves the qualitative floor: does
the program halt at all, over every input. [Worst-case execution-time
analysis](https://quality.stereobooster.com/wcet-analysis.md) assumes it halts and proves a sound *upper*
bound on running time for the modeled hardware. [Algorithmic complexity
testing](https://quality.stereobooster.com/algorithmic-complexity.md) trades proof for search: it hunts an
input that drives cost past its expected growth, witnessing a *lower* bound on how bad
the worst case gets.

Termination is the precondition, since a runtime that might be infinite has no bound to
compute. WCET and complexity testing then bracket the same worst case from opposite
sides: WCET over-approximates (sound, never optimistic, sometimes pessimistic), while
complexity testing under-approximates (a blow-up it finds is real, but finding none
proves nothing). The two sound static methods and the one empirical search are the
formal and the testing answers to a single question about resource use.

## Classification

- **Quality dimensions:** Functionality: safety, Reliability (proves the liveness property that a program halts — a hang or runaway loop is an availability failure).
- **Area:** Real-time and reactive systems that must guarantee a response, OS and driver loops, smart contracts, total functional programming; anywhere a hang or runaway loop is a failure, not just a slowdown.
- **Guarantee:** Exhaustive — when the analysis succeeds it proves termination over all inputs; sound but incomplete, since termination is undecidable.

## Referenced by

- [Formal methods](https://quality.stereobooster.com/formal.md) · Methods
- [Verifying numerical code](https://quality.stereobooster.com/numbers.md) · Methods
- [Worst-case execution-time analysis](https://quality.stereobooster.com/wcet-analysis.md) · Methods
- [Glossary](https://quality.stereobooster.com/glossary.md) · Overview

## References

[^cook2011]: Cook, Byron, Andreas Podelski, and Andrey Rybalchenko. 2011. "[Proving Program Termination](https://www.cs.umd.edu/users/gasarch/TOPICS/ramsey/provingtermination.pdf)." *Communications of the ACM* 54 (5): 88–98. <https://doi.org/10.1145/1941487.1941509>.

## Acronyms

- WCET — worst-case execution time