Skip to Main content Skip to Navigation
Conference papers

An abstract domain to infer ordinal-valued ranking functions

Caterina Urban 1, 2 Antoine Miné 1, 2
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
2 Abstraction
LIENS - Laboratoire d'informatique de l'école normale supérieure
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 maximum degree of the polynomial, and the types of functions used as polynomial coefficients. We have implemented a prototype static analyzer for a while-language by instantiating our domain using affine functions as polynomial coefficients. We successfully analyzed small but intricate examples that are out of the reach of existing methods. 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 subsumes existing techniques based on lexicographic ranking functions.
Complete list of metadatas
Contributor : Antoine Miné <>
Submitted on : Wednesday, January 8, 2014 - 2:50:52 PM
Last modification on : Tuesday, September 22, 2020 - 3:51:19 AM

Links full text




Caterina Urban, Antoine Miné. An abstract domain to infer ordinal-valued ranking functions. ESOP 2014 - 23rd European Symposium on Programming, Apr 2014, Grenoble, France. pp.412-431, ⟨10.1007/978-3-642-54833-8_22⟩. ⟨hal-00925731⟩



Record views