Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Ströder, T.; Giesl, J.; Brockschmidt, M.; Frohn, F.; Fuhs, Carsten; Hensel, J.; Schneider-Kamp, P.; Aschermann, C. (2017)
Publisher: Springer
Languages: English
Types: Article
Subjects: Termination, csis, C programs, LLVM, Symbolic Execution, Memory Safety

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.

  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 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: http://aprove.informatik.rwth-aachen.de/eval/PointerJournal/.
    • 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.
    • 11. M. Brockschmidt, C. Otto, C. von Essen, and J. Giesl. Termination graphs for Java Bytecode. In Verification, Induction, Termination Analysis, LNAI 6463, 2010.
    • 12. M. Brockschmidt, C. Otto, and J. Giesl. Modular termination proofs of recursive Java Bytecode programs by term rewriting. In Proc. RTA '11.
    • 13. M. Brockschmidt, T. Str o¨der, C. Otto, and J. Giesl. Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In Proc. FoVeOOS '11.
    • 14. M. Brockschmidt, R. Musiol, C. Otto, and J. Giesl. Automated termination proofs for Java programs with cyclic data. In Proc. CAV '12.
    • 15. M. Brockschmidt, B. Cook, and C. Fuhs. Better termination proving through cooperation. In Proc. CAV '13.
    • 16. J. Brotherston and N. Gorogiannis. Cyclic abduction of inductively defined safety and termination preconditions. In Proc. SAS '14.
    • 17. D. Cachera and D. Pichardie. A certified denotational abstract interpreter. In Proc. ITP '10.
    • 18. C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. OSDI '08.
    • 19. C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In Proc. SAS '06.
    • 20. C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang. Space invading systems code. In Proc. LOPSTR '08.
    • 21. C. Calcagno and D. Distefano. Infer: An automatic program verifier for memory safety of C programs. In Proc. NFM '11.
    • 22. H. Y. Chen, C. David, D. Kroening, P. Schrammel, and N. Wa¨chter. Synthesising interprocedural bitprecise termination proofs. In Proc. ASE '15.
    • 23. Clang compiler: http://clang.llvm.org.
    • 24. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752-794, 2003.
    • 25. E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain. Automated certified proofs with CiME3. In Proc. RTA '11.
    • 26. B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In Proc. SAS '05.
    • 27. B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In Proc. PLDI '06.
    • 28. B. Cook, A. Podelski, and A. Rybalchenko. Summarization for termination: no return! Formal Methods in System Design, 35(3):369-387, 2009.
    • 29. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. POPL '78.
    • 30. C. David, D. Kroening, and M. Lewis. Unrestricted termination and non-termination arguments for bit-vector programs. In Proc. ESOP '15.
    • 31. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. TACAS '08.
    • 32. V. D'Silva and C. Urban. Conflict-driven conditional termination. In Proc. CAV '15.
    • 33. K. Dudka, P. Peringer, and T. Vojnar. Predator: A shape analyzer based on symbolic memory graphs (competition contribution). In Proc. TACAS '14.
    • 34. B. Dutertre and L. de Moura. The Yices SMT solver. Tool paper at http://yices.csl.sri.com/ tool-paper.pdf.
    • 35. S. Falke, D. Kapur, and C. Sinz. Termination analysis of C programs using compiler intermediate languages. In Proc. RTA '11.
    • 36. S. Falke, F. Merz, and C. Sinz. LLBMC: Improved bounded model checking of C using LLVM (competition contribution). In Proc. TACAS '13.
    • 37. C. Fuhs, J. Giesl, M. Pl u¨cker, P. Schneider-Kamp, and S. Falke. Proving termination of integer term rewriting. In Proc. RTA '09.
    • 38. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Pl u¨cker, P. Schneider-Kamp, T. Stro¨der, S. Swiderski, and R. Thiemann. Proving termination of programs automatically with AProVE. In Proc. IJCAR '14.
    • 39. L. Gonnord, D. Monniaux, and G. Radanne. Synthesis of ranking functions using extremal counterexamples. In Proc. PLDI '15.
    • 40. S. Gulwani and A. Tiwari. An abstract domain for analyzing heap-manipulating low-level software. In Proc. CAV '07.
    • 41. P. Habermehl, R. Iosif, A. Rogalewicz, and T. Vojnar. Proving termination of tree manipulating programs. In Proc. ATVA '07.
    • 42. W. R. Harris, A. Lal, A. Nori, and S. K. Rajamani. Alternation for termination. In Proc. SAS '10.
    • 43. M. Heizmann, J. Hoenicke, J. Leike, and A. Podelski. Linear ranking for linear lasso programs. In Proc. ATVA '13.
    • 44. J. Hensel, J. Giesl, F. Frohn, and T. Stro¨der. Proving termination of programs with bitvector arithmetic by symbolic execution. In Proc. SEFM '16.
    • 45. R. Iosif and A. Rogalewicz. Automata-based termination proofs. Comp. and Inf., 32(4):739-775, 2013.
    • 46. J.-H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie. A formally-verified C static analyzer. In Proc. POPL '15.
    • 47. C. Kop and N. Nishida. Automatic constrained rewriting induction towards verifying procedural programs. In Proc. APLAS '14.
    • 48. C. Kop and N. Nishida. Constrained Term Rewriting tooL. In Proc. LPAR '15.
    • 49. D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination analysis with compositional transition invariants. In Proc. CAV '10.
    • 50. D. Larraz, A. Oliveras, E. Rodr´ıguez-Carbonell, and A. Rubio. Proving termination of imperative programs using Max-SMT. In Proc. FMCAD '13.
    • 51. C. Lattner and V. S. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proc. CGO '04.
    • 52. T. C. Le, S. Qin, and W. Chin. Termination and non-termination specification inference. In Proc. PLDI '15.
    • 53. LLVM reference manual. http://llvm.org/docs/LangRef.html.
    • 54. S. Lo¨we, M. Mandrykin, and P. Wendler. CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In Proc. TACAS '14.
    • 55. S. Magill. Instrumentation Analysis: An Automated Method for Producing Numeric Abstractions of Heap-Manipulating Programs. PhD thesis, CMU, Pittsburgh, PA, USA, 2010. Available at http://www. cs.cmu.edu/~smagill/papers/thesis.pdf.
    • 56. S. Magill, M. Tsai, P. Lee, and Y. Tsay. Automatic numeric abstractions for heap-manipulating programs. In Proc. POPL '10.
    • 57. A. Mine´. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31-100, 2006.
    • 58. Y. Moy and C. Marche´. Modular inference of subprogram contracts for safety checking. J. Symb. Comput., 45(11), 2010.
    • 59. R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 53(6), 2006.
    • 60. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002.
    • 61. P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Proc. CSL '01.
    • 62. http://fxr.watson.org/fxr/source/lib/libsa/strlen.c?v=OPENBSD.
    • 63. C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated termination analysis of Java Bytecode by term rewriting. In Proc. RTA '10.
    • 64. A. Podelski and A. Rybalchenko. ARMC: The logical choice for software model checking with abstraction refinement. In Proc. PADL '07.
    • 65. T. W. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proc. POPL '95.
    • 66. F. Spoto, F. Mesnard, and E´. Payet. A termination analyser for Java Bytecode based on path-length. ACM TOPLAS, 32(3), 2010.
    • 67. T. Stro¨der, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. Schneider-Kamp. Proving termination and memory safety for programs with pointer arithmetic. In Proc. IJCAR '14.
    • 68. T. Stro¨der, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl. AProVE: Termination and memory safety of C programs (competition contribution). In Proc. TACAS '15.
    • 69. R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In Proc. TPHOLs '09.
    • 70. A. Tsitovich, N. Sharygina, C. M. Wintersteiger, and D. Kroening. Loop summarization and termination analysis. In Proc. TACAS '11.
    • 71. C. Urban, A. Gurfinkel, and T. Kahsai. Synthesizing ranking functions from bits and pieces. In Proc. TACAS '16.
    • 72. Wikibooks C Programming: http://en.wikibooks.org/wiki/C_Programming/.
    • 73. J. Zhao, S. Nagarakatte, M. M. K. Martin, and S. Zdancewic. Formalizing the LLVM IR for verified program transformations. In Proc. POPL '12.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article