一句话：提出面向C程序的位精确过程模块化终止性分析，通过模板化过程间摘要结合前向过近似与终止前置条件欠近似推断。
非终止是挂起程序和拒绝服务漏洞等缺陷的根源，自动化证明其不存在十分必要。现有终止分析多聚焦于单过程的小规模问题，难以扩展到大型系统。本文提出一种基于模板化过程间摘要的模块化终止分析：将上下文敏感的前向过近似分析与终止前置条件的欠近似推断相结合，并在字典序线性ranking function模板上合成位精确的终止性论证。实验表明，过程间推理在效率上优于整体式分析，同时保持相当的精度。
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.
@article{ChenDKSW18,
title = {Bit-Precise Procedure-Modular Termination Analysis},
author = {Hong-Yi Chen and Cristina David and Daniel Kroening and Peter Schrammel and Björn Wachter},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {1},
year = {2017},
doi = {10.1145/3121136}
}