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.
Type de document :
Communication dans un congrès
Zhong Shao. ESOP 2014 - 23rd European Symposium on Programming, Apr 2014, Grenoble, France. Springer, 8410, pp.412-431, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-642-54833-8_22〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00925731
Contributeur : Antoine Miné <>
Soumis le : mercredi 8 janvier 2014 - 14:50:52
Dernière modification le : mardi 17 avril 2018 - 11:25:23

Lien texte intégral

Identifiants

Collections

Citation

Caterina Urban, Antoine Miné. An abstract domain to infer ordinal-valued ranking functions. Zhong Shao. ESOP 2014 - 23rd European Symposium on Programming, Apr 2014, Grenoble, France. Springer, 8410, pp.412-431, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-642-54833-8_22〉. 〈hal-00925731〉

Partager

Métriques

Consultations de la notice

409