Termination analysis and call graph construction for higher-order functional programs
Termination analysis and call graph construction for higher-order functional programs
复制标题
高阶函数程序的终止分析和调用图构建
DOI：
10.1145/1291220.1291165
复制
发表时间：
2007
影响因子：
--
通讯作者：
Sereni D
中科院分区：
文献类型：
--
作者：
Sereni D
高阶程序的分析和验证提出了高阶语言的控制流分析问题。为高阶程序构建准确的调用图的问题一直是广泛研究的主题，并提出了许多复杂性和精确度不同的流分析方法。虽然已经研究了高阶程序的终止分析，但很少研究调用图构造对终止检查精度的影响。我们研究了各种控制流分析技术对高阶函数程序的终止分析的影响。我们提出了一个终止检查框架，并实例化这三个调用图的结构不同的精度和复杂性，并举例说明了调用图construction.Our的第二个目标的选择的影响是使用由此产生的分析，揭示控制流分析之间的关系。我们证明了精确的包含类之间的程序确认为终止相同的终止标准在不同的调用图分析，给出了第一个表征的表达能力的流分析高阶程序。
The analysis and verification of higher-order programs raises the issue of control-flow analysis for higher-order languages. The problem of constructing an accurate call graph for a higher-order program has been the topic of extensive research, and numerous methods for flow analysis, varying in complexity and precision, have been suggested.While termination analysis of higher-order programs has been studied, there has been little examination of the impact of call graph construction on the precision of termination checking. We examine the effect of various control-flow analysis techniques on a termination analysis for higher-order functional programs. We present a termination checking framework and instantiate this with three call graph constructions varying in precision and complexity, and illustrate by example the impact of the choice of call graph construction.Our second aim is to use the resulting analyses to shed light on the relationship between control-flow analyses. We prove precise inclusions between the classes of programs recognised as terminating by the same termination criterion over different call graph analyses, giving one of the first characterisations of expressive power of flow analyses for higher-order programs.
登录
查看更多内容
使用 AProVE 自动终止证明
DOI：
--
发表时间：
2004
期刊：
International Conference on Rewriting Techniques and Applications
影响因子：
--
作者：
J. Giesl;René Thiemann;Peter Schneider;Stephan Falke
通讯作者：
Stephan Falke
高阶函数程序的关系抽象解释（扩展摘要）
DOI：
--
发表时间：
1991
期刊：
JTASPEFT/WSA
影响因子：
--
作者：
P. Cousot;R. Cousot
通讯作者：
R. Cousot
DOI：
10.1007/11817963_37
发表时间：
2006-01-01
期刊：
COMPUTER AIDED VERIFICATION, PROCEEDINGS
影响因子：
--
作者：
Cook, Byron;Podelski, Andreas;Rybalchenko, Andrey
通讯作者：
Rybalchenko, Andrey
DOI：
--
发表时间：
1996
期刊：
影响因子：
--
作者：
Naomi Lindenstrauss;Y. Sagiv
通讯作者：
Y. Sagiv
DOI：
--
发表时间：
2005
期刊：
Asian Symposium on Programming Languages and Systems
影响因子：
--
作者：
D. Sereni;N. Jones
通讯作者：
N. Jones