The following technical report is available from
http://aib.informatik.rwth-aachen.de:
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, and Cornelius Aschermann
AIB 2016-09
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.
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)