Skip to main content
SpringerLink
Log in

Algorithmic Analysis of Array-Accessing Programs

  • Conference paper
Computer Science Logic (CSL 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5771))

Included in the following conference series:

Abstract

For programs whose data variables range over boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, we consider algorithmic verification of programs that use boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over a potentially unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly-nested loops. The second result establishes connections to automata and logics defining languages over data words.

This research was partially supported by NSF Cybertrust award CNS 0524059.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Alur, R., Černý, P., Weinstein, S.: Algorithmic analysis of array-accessing programs. Technical Report MS-CIS-08-35. University of Pennsylvania (2008)

    Google Scholar 

  2. Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 164–180. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1–3 (2002)

    Google Scholar 

  4. Björklund, H., Bojańczyk, M.: Shuffle expressions and words with nested data. In: Kučera, L., Kučera, A. (eds.) MFCS 2007. LNCS, vol. 4708, pp. 750–761. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Björklund, H., Schwentick, T.: On notions of regularity for data languages. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 88–99. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS, pp. 7–16 (2006)

    Google Scholar 

  7. Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 1–22. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. In: LICS, pp. 17–26 (2006)

    Google Scholar 

  10. Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: ICDT, pp. 252–267 (2009)

    Google Scholar 

  11. Gischer, J.: Shuffle languages, Petri nets, and context-sensitive grammars. Commun. ACM 24(9), 597–605 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  12. Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL, pp. 338–350 (2008)

    Google Scholar 

  13. Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72–83 (1997)

    Google Scholar 

  14. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235–246 (2008)

    Google Scholar 

  15. Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science 134(2), 329–363 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  18. Lazić, R.: Decidability of reachability for polymorphic systems with arrays: A complete classification. ENTCS 138(3), 3–19 (2005)

    MathSciNet  MATH  Google Scholar 

  19. Lipton, R.: The reachability problem requires exponential space. Technical Report Dept. of Computer Science, Research report 62. Yale University (1976)

    Google Scholar 

  20. Minski, M.: Recursive unsolvability of Post’s problem of ’tag’ and other topics in theory of Turing machines. Annals of Mathematics 74, 437–455 (1962)

    Article  MathSciNet  Google Scholar 

  21. Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5(3), 403–435 (2004)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Pennsylvania, USA

    Rajeev Alur, Pavol Černý & Scott Weinstein

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pavol Černý
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Scott Weinstein
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematische Grundlagen der Informatik, RWTH Aachen, 52056, Aachen, Germany

    Erich Grädel

  2. CENTRIA and Departamento de Matemática, Universidade Nova de Lisboa, 2829-516, Caparica, Portugal

    Reinhard Kahle

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Černý, P., Weinstein, S. (2009). Algorithmic Analysis of Array-Accessing Programs. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04027-6_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04026-9

  • Online ISBN: 978-3-642-04027-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation