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