To Infinity... and Beyond!

Caterina Urban 1 Antoine Miné 1
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
Abstract : The traditional method for proving program termination consists in inferring a ranking function. In many cases (i.e. programs with unbounded non-determinism), a single ranking function over natural numbers is not sufficient. Hence, we propose a new abstract domain to automatically infer ranking functions over ordinals. We extend an existing domain for piecewise-defined natural-valued ranking functions to polynomials in ω, where the polynomial coefficients are natural-valued functions of the program variables. The abstract domain is parametric in the choice of the state partitioning inducing the piecewise-definition and the type of functions used as polynomial coefficients. To our knowledge this is the first abstract domain able to reason about ordinals. Handling ordinals leads to a powerful approach for proving termination of imperative programs, which in particular allows us to take a first step in the direction of proving termination under fairness constraints and proving liveness properties of (sequential and) concurrent programs.
Document type :
Conference papers
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01105216
Contributor : Antoine Miné <>
Submitted on : Tuesday, January 20, 2015 - 3:31:54 PM
Last modification on : Thursday, February 7, 2019 - 3:49:17 PM
Long-term archiving on : Tuesday, April 21, 2015 - 10:11:07 AM

File

article-urban-mine-wst14.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01105216, version 1

Collections

Citation

Caterina Urban, Antoine Miné. To Infinity... and Beyond!. 14th International Workshop on Termination (WST'14), Jul 2014, Vienne, Austria. pp.5. ⟨hal-01105216⟩

Share

Metrics

Record views

362

Files downloads

190