Bit-Precise Procedure-Modular Termination Analysis
Bit-Precise Procedure-Modular Termination Analysis
复制标题
DOI：
10.1145/3121136
复制
发表时间：
2018-01-01
影响因子：
1.3
通讯作者：
Wachter, Bjoern
中科院分区：
文献类型：
--
作者：
Chen, Hong-Yi;David, Cristina;Wachter, Bjoern
非终止性是各种程序错误的根本原因，例如挂起程序和拒绝服务漏洞。这使得可以证明不存在此类错误的自动分析非常可取。为了将终止检查扩展到大型系统，过程间终止分析似乎是必不可少的。这是一个在很大程度上未开发的研究领域，在终止分析，其中大部分的努力都集中在小，但困难的单程序problems.We提出了一个模块化的终止分析C程序使用基于模板的过程间的总结。我们的分析结合了上下文敏感的，过度近似的前向分析与推断下近似终止的前提条件。位精确的终止参数是在字典式线性排名函数模板上合成的。我们的实验结果表明，跨过程推理的优势，整体分析的效率，同时保持相当的精度。
Non-termination is the root cause of a variety of program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedural termination analysis seems essential. This is a largely unexplored area of research in termination analysis, where most effort has focussed on small but difficult single-procedure problems.We present a modular termination analysis for C programs using template-based interprocedural summarisation. Our analysis combines a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination. Bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. Our experimental results show the advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.