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程序（含内存分配和显式指针运算）终止性分析的强大技术扩展至列表场景。