• AIB 2016-09: Automatically Proving Termination and Memory Safety for Pr

    From Jera Hensel@21:1/5 to All on Wed Sep 28 19:23:54 2016
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)