Skip to main content
SpringerLink
Log in

Proving Termination and Memory Safety for Programs with Pointer Arithmetic

  • Conference paper
Automated Reasoning (IJCAR 2014)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8562))

Included in the following conference series:

Abstract

Proving termination automatically for programs with explicit pointer arithmetic is 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 represents all possible runs of the 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.

Supported by DFG grant GI 274/6-1 and Research Training Group 1298 (AlgoSyn).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 2–18. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  2. AProVE, http://aprove.informatik.rwth-aachen.de/eval/Pointer/

  3. Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for JBC. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123–141. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  5. Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 105–122. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350–367. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. Clang compiler, http://clang.llvm.org

  9. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL 1977, pp. 238–252. ACM Press (1977)

    Google Scholar 

  10. Dudka, K., Peringer, P., Vojnar, T.: Predator: A shape analyzer based on symbolic memory graphs (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 412–414. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  11. Dutertre, B., de Moura, L.M.: The Yices SMT solver (2006), http://yices.csl.sri.com/tool-paper.pdf

  12. Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schauß, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 41–50. Dagstuhl Publishing (2011)

    Google Scholar 

  13. Falke, S., Merz, F., Sinz, C.: LLBMC: Improved bounded model checking of C using LLVM (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 623–626. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  14. Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304–319. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365–380. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89–103. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75–88. IEEE (2004)

    Google Scholar 

  18. Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 392–394. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  19. Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Automatic numeric abstractions for heap-manipulating programs. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL 2010, pp. 211–222. ACM Press (2010)

    Google Scholar 

  20. de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Moy, Y., Marché, C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput. 45(11), 1184–1211 (2010)

    Article  MATH  Google Scholar 

  22. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Google Scholar 

  23. http://fxr.watson.org/fxr/source/lib/libsa/strlen.c?v=OPENBSD

  24. Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS 32(3) (2010)

    Google Scholar 

  26. Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Automated termination analysis for programs with pointer arithmetic. Tech. Rep. AIB 2014-05 available from [2] and from http://aib.informatik.rwth-aachen.de

  27. SV-COMP at TACAS 2014, http://sv-comp.sosy-lab.org/2014/

  28. Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81–95. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  29. Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 43–62. Springer, Heidelberg (2013)

    Google Scholar 

  30. Wikibooks C Programming, http://en.wikibooks.org/wiki/C_Programming/

  31. Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM IR for verified program transformations. In: Field, J., Hicks, M. (eds.) POPL 2012, pp. 427–440. ACM Press (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LuFG Informatik 2, RWTH Aachen University, Germany

    Thomas Ströder, Jürgen Giesl, Florian Frohn & Jera Hensel

  2. Microsoft Research Cambridge, UK

    Marc Brockschmidt

  3. Dept. of Computer Science, University College London, UK

    Carsten Fuhs

  4. IMADA, University of Southern Denmark, Denmark

    Peter Schneider-Kamp

Authors
  1. Thomas Ströder
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marc Brockschmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Florian Frohn
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Carsten Fuhs
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Jera Hensel
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Peter Schneider-Kamp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS,, New York University &amp, USA

    Stéphane Demri

  2. Department of Computer Science, University of New Mexico, 87131-0001, Albuquerque, NM, USA

    Deepak Kapur

  3. Max Planck Institute for Informatics, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Ströder, T. et al. (2014). Proving Termination and Memory Safety for Programs with Pointer Arithmetic. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08587-6_15

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08586-9

  • Online ISBN: 978-3-319-08587-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation