Piecewise-Defined Ranking Functions

Caterina Urban 1, 2
1 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
2 Abstraction
LIENS - Laboratoire d'informatique de l'école normale supérieure
Abstract : We present the design and implementation of an abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis is sound, meaning that all program executions respecting these sufficient conditions are indeed terminating. We discuss the limitations of the proposed framework, and we investigate possible future work. In particular, we explore potential extensions of the abstract domain considering piecewise-defined non-linear ranking functions such as polynomials or exponentials.
Type de document :
Communication dans un congrès
Johannes Waldmann. 13th International Workshop on Termination, Aug 2013, Bertinoro, Italy. pp.69-73, 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00925682
Contributeur : Antoine Miné <>
Soumis le : mercredi 8 janvier 2014 - 14:16:39
Dernière modification le : jeudi 11 janvier 2018 - 06:26:23

Identifiants

  • HAL Id : hal-00925682, version 1

Collections

Citation

Caterina Urban. Piecewise-Defined Ranking Functions. Johannes Waldmann. 13th International Workshop on Termination, Aug 2013, Bertinoro, Italy. pp.69-73, 2013. 〈hal-00925682〉

Partager

Métriques

Consultations de la notice

133