Automatically proving termination and memory safety for programs with pointer arithmetic

Article English OPEN
Ströder, T. ; Giesl, J. ; Brockschmidt, M. ; Frohn, F. ; Fuhs, Carsten ; Hensel, J. ; Schneider-Kamp, P. ; Aschermann, C. (2017)
  • Publisher: Springer
  • Related identifiers: doi: 10.1007/s10817-016-9389-x
  • Subject: Termination | csis | C programs | LLVM | Symbolic Execution | Memory Safety

<p>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.</p>
  • References (73)
    73 references, page 1 of 8

    1. A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik. Ufo: A framework for abstraction- and interpolation-based software verification. In Proc. CAV '12.

    2. E. Albert, P. Arenas, M. Codish, S. Genaim, G. Puebla, and D. Zanardini. Termination analysis of Java Bytecode. In Proc. FMOODS '08.

    3. AProVE:

    4. J. Berdine, B. Cook, D. Distefano, and P. W. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In Proc. CAV '06.

    5. J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O'Hearn. Variance analyses from invariance analyses. In Proc. POPL '07.

    6. J. Berdine, B. Cook, and S. Ishtiaq. SLAyer: Memory safety for systems-level code. In Proc. CAV '11.

    7. Y. Bertot and P. Caste´ran. CoqArt. Springer, 2004.

    8. F. Blanqui and A. Koprowski. CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Structures in Comp. Sc., 4:827-859, 2011.

    9. M. Bodin, T. Jensen, and A. Schmitt. Certified abstract interpretation with pretty-big-step semantics. In Proc. CPP '15.

    10. A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. Formal Methods in System Design, 38(2):158-192, 2011.

  • Metrics
    No metrics available
Share - Bookmark