Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

The work

TitleAutomatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
AuthorsThomas Ströder; Jürgen Giesl; Marc Brockschmidt; Florian Frohn; Carsten Fuhs; Jera Hensel; Peter Schneider-Kamp; Cornelius Aschermann
Typearticle
Year2017
Citekeystroder2017automatically

Where it appeared

Published inJournal of Automated Reasoning
PublisherSpringer
Volume58
Issue1
Pages33--65

Identifiers

DOI10.1007/s10817-016-9389-x
OpenAlexW2536541088

Access

Landing pagehttps://doi.org/10.1007/s10817-016-9389-x
Free full texthttps://findresearcher.sdu.dk/ws/files/141379199/Automatically_Proving_Termination_and_Memory_Safety_for_Programs_with_Pointer_Arithmetic.pdf

Abstract

While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic fully automatically was still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that over-approximates all possible runs of a program and that can be used to prove memory safety. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.

Copy held

KindPDF, 561.0 kB
Retrieved2026-08-08
Heldlocal, for personal reference
Opens atpage 2
Where it came fromhttps://doi.org/10.1007/s10817-016-9389-x

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-05
Recordreviewed by a person
Approved2026-08-16
In: Journal of Automated Reasoning venue Separation logic topic

Cite it as

@article{stroder2017automatically,
  title = {Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic},
  author = {Thomas Ströder and Jürgen Giesl and Marc Brockschmidt and Florian Frohn and Carsten Fuhs and Jera Hensel and Peter Schneider-Kamp and Cornelius Aschermann},
  year = {2017},
  journal = {Journal of Automated Reasoning},
  volume = {58},
  number = {1},
  pages = {33--65},
  publisher = {Springer},
  doi = {10.1007/s10817-016-9389-x},
  url = {https://findresearcher.sdu.dk/ws/files/141379199/Automatically_Proving_Termination_and_Memory_Safety_for_Programs_with_Pointer_Arithmetic.pdf},
}

This record lives at https://refs.drheap.org/stroder2017automatically/ and will keep doing so.