Advertisement

Abstract

In this paper we analyze the complexity of checking safety and termination properties, for a very simple, yet non-trivial, class of programs with singly-linked list data structures. Since, in general, programs with lists are known to have the power of Turing machines, we restrict the control structure, by forbidding nested loops and destructive updates. Surprisingly, even with these simplifying conditions, verifying safety and termination for programs working on heaps with more than one cycle are undecidable, whereas decidability can be established when the input heap may have at most one loop. The proofs for both the undecidability and the decidability results rely on non-trivial number-theoretic results.

Keywords

Nest Loop Reachability Problem Predicate Abstraction List Program Root Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Balaban, I., Pnueli, A., Zuck, L.: Shape Analysis by Predicate Abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 17–19. Springer, Heidelberg (2005)Google Scholar
  2. 2.
    Bardin, S., Finkel, A., Nowak, D.: Toward Symbolic Verification of Programs Handling Pointers. AVIS. Barcelona, Spain (2004)Google Scholar
  3. 3.
    Bardin, S., Finkel, A., Lozes, E., Sangnier, A.: From pointer systems to counter systems using shape analysis. In: 5th International Workshop on Automated Verification of Infinite-State Systems, AVIS (2006)Google Scholar
  4. 4.
    Beltyukov, A.P.: Decidability of the universal theory of natural numbers with addition and divisibility. Zapiski Nauch. Sem. Leningrad Otdeleniya Mathematical Institute 60, 15–28 (1976)Google Scholar
  5. 5.
    Berdine, J., Calcagno, C., O’Hearn, P.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, Springer, Heidelberg (2004)Google Scholar
  6. 6.
    Bés, A.: A survey of arithmetical definability. A Tribute to Maurice Boffa. Bulletin de la Société Mathématique de Belgique, 1–54 (2002)Google Scholar
  7. 7.
    Boigelot, B.: On iterating linear transformations over recognizable sets of integers. TCS 309(2), 413–468 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Bouajjani, A., et al.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Technical Report TR-2006-3, VERIMAG (2006)Google Scholar
  10. 10.
    Bouajjani, A., et al.: Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)Google Scholar
  11. 11.
    Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 425–439. Springer, Heidelberg (2005)Google Scholar
  12. 12.
    Chakaravarthy, V.T.: New results on the computability and complexity of points-to-analysis. In: International Conference on Principles of Programming Languages, POPL (2003)Google Scholar
  13. 13.
    Church, A.: An unsolvable problem of elementary number theory. American Journal of Mathematics 58, 345–363 (1936)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Comon, H., Jurski, Y.: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  15. 15.
    Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 173–198 (1931)zbMATHCrossRefGoogle Scholar
  17. 17.
    Ishtiaq, S., O’Hearn, P.: BI as an assertion language for mutable data structures. In: POPL (2001)Google Scholar
  18. 18.
    Lipshitz, L.: The diophantine problem for addition and divisibility. Transaction of the American Mathematical Society 235, 271–283 (1976)CrossRefMathSciNetGoogle Scholar
  19. 19.
    Manevich, R., et al.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)Google Scholar
  20. 20.
    Matiyasevich, Y.: Enumerable sets are diophantine. Journal of Sovietic Mathematics 11, 354–358 (1970)zbMATHGoogle Scholar
  21. 21.
    Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: PLDI (2001)Google Scholar
  22. 22.
    Presburger, M.: Über die Vollstandigkeit eines gewissen Systems der Arithmetik. In: Comptes rendus du I Congrés des Pays Slaves, Warsaw (1929)Google Scholar
  23. 23.
    Robinson, J.: Definability and decision problems in arithmetic. The Journal of Symbolic Logic 14(2), 98–114 (1949)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. In: TOPLAS (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Marius Bozga
    • 1
  • Radu Iosif
    • 1
  1. 1.VERIMAG, 2 av. de Vignate, F-38610 Gières 

Personalised recommendations