Automated Termination Proofs for C Programs with Lists (Short WST Version)

TL;DR

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

Contribution

It is the first method to adapt powerful termination analysis techniques specifically for C programs with recursive data structures such as lists.

Findings

Extends termination analysis techniques to list-manipulating C programs.

Handles memory allocation and pointer arithmetic in termination proofs.

Provides a new tool for verifying termination in complex C programs.

Abstract

There are many techniques and tools for termination of C programs, but up to now they were not very powerful for 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.