Proving Termination of C Programs with Lists
Logic in Computer Science
2023-06-06 v2
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.
Cite
@article{arxiv.2305.12159,
title = {Proving Termination of C Programs with Lists},
author = {Jera Hensel and Jürgen Giesl},
journal= {arXiv preprint arXiv:2305.12159},
year = {2023}
}
Comments
Full version of a paper which appeared in the Proceedings of CADE 2023