Paper Info
Title
An Abstract Domain to Infer Ordinal-Valued Ranking Functions.
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.
Year
DOI
Venue
2014
10.1007/978-3-642-54833-8_22
Lecture Notes in Computer Science
Field
DocType
Volume
Affine transformation,Natural number,Polynomial,Ranking,Computer science,Ordinal number,Theoretical computer science,Parametric statistics,Degree (graph theory),Lexicographical order
Conference
8410
ISSN
Citations 
PageRank 
0302-9743
18
0.69
References 
Authors
16
2
Name
Order
Citations
PageRank
Caterina Urban1795.39
Antoine Miné2111751.15