Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

Thomas Ströder, Jürgen Giesl*, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp, Cornelius Aschermann

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

87 Downloads (Pure)

Resumé

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.

OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind58
Udgave nummer1
Sider (fra-til)33-65
ISSN0168-7433
DOI
StatusUdgivet - 2017

Fingeraftryk

Data storage equipment

Citer dette

Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., ... Aschermann, C. (2017). Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. Journal of Automated Reasoning, 58(1), 33-65. https://doi.org/10.1007/s10817-016-9389-x
Ströder, Thomas ; Giesl, Jürgen ; Brockschmidt, Marc ; Frohn, Florian ; Fuhs, Carsten ; Hensel, Jera ; Schneider-Kamp, Peter ; Aschermann, Cornelius. / Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. I: Journal of Automated Reasoning. 2017 ; Bind 58, Nr. 1. s. 33-65.
@article{ee3f02db11e64086b9e6ee671714fd71,
title = "Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic",
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.",
keywords = "C programs, LLVM, Memory Safety, Symbolic Execution, Termination",
author = "Thomas Str{\"o}der and J{\"u}rgen Giesl and Marc Brockschmidt and Florian Frohn and Carsten Fuhs and Jera Hensel and Peter Schneider-Kamp and Cornelius Aschermann",
year = "2017",
doi = "10.1007/s10817-016-9389-x",
language = "English",
volume = "58",
pages = "33--65",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer",
number = "1",

}

Ströder, T, Giesl, J, Brockschmidt, M, Frohn, F, Fuhs, C, Hensel, J, Schneider-Kamp, P & Aschermann, C 2017, 'Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic', Journal of Automated Reasoning, bind 58, nr. 1, s. 33-65. https://doi.org/10.1007/s10817-016-9389-x

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. / Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius.

I: Journal of Automated Reasoning, Bind 58, Nr. 1, 2017, s. 33-65.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

AU - Ströder, Thomas

AU - Giesl, Jürgen

AU - Brockschmidt, Marc

AU - Frohn, Florian

AU - Fuhs, Carsten

AU - Hensel, Jera

AU - Schneider-Kamp, Peter

AU - Aschermann, Cornelius

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - C programs

KW - LLVM

KW - Memory Safety

KW - Symbolic Execution

KW - Termination

U2 - 10.1007/s10817-016-9389-x

DO - 10.1007/s10817-016-9389-x

M3 - Journal article

VL - 58

SP - 33

EP - 65

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1

ER -