摘要：将C程序的终止方法证明为一个经常被使用的技术和工具，然而直到现在，这些工具对于依赖于递归数据结构（如列表）的程序的全自动终止证明并不是很强大。我们提出了第一个方法，将强大的C程序终止分析技术（包括内存分配和显式指针运算）扩展到列表。
作者：Jera Hensel, J"urgen Giesl
论文ID：2305.12159
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-06
PDF 下载： 英文版 中文版pdf翻译中