There are many techniques and tools to prove termination of C programs, but up to now these tools were not very powerful for fully automated termination proofs of programs whose termination depends on recursive data structures like lists. We present the first approach that extends powerful techniques for termination analysis of C programs (with memory allocation and explicit pointer arithmetic) to lists.

翻译：有许多技术和工具可用于证明C程序的终止性，但迄今为止，对于终止性依赖于递归数据结构（如列表）的程序，这些工具在全自动终止性证明方面并不十分强大。我们提出了第一种方法，将用于C程序（含内存分配和显式指针算术）终止性分析的强大技术扩展到列表。