An Abstract Domain to Infer Ordinal-Valued Ranking Functions
An Abstract Domain to Infer Ordinal-Valued Ranking Functions
复制标题
推断序数值排序函数的抽象域
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
A. Miné
中科院分区：
文献类型：
--
作者：
Caterina Urban;A. Miné
传统的方法终止的方法是在许多情况下推断出无界非确定性的程序，而对自然数的单个排名函数是不够的。普通人。
我们将分段定义的自然价值排名函数扩展到ω中的多项式，其中多项式系数是程序变量的自然值函数。用作多项式系数的功能的类型。
我们通过使用仿射函数作为多项式系数实例化域来实现我们的域名原型静态分析仪。
据我们所知，这是第一个能够推理普通人的抽象领域。
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.