Proving Termination of C Programs with Lists

TL;DR

This paper introduces a novel approach for automatically proving the termination of C programs that manipulate recursive data structures like lists, extending existing techniques to handle memory and pointers.

Contribution

It is the first method to adapt advanced termination analysis techniques to C programs with lists, enabling more automated proofs.

Findings

Extends termination analysis techniques to list-manipulating C programs

Supports programs with memory allocation and pointer arithmetic

Enables more automated termination proofs for complex data structures

Abstract

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.