Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs

  • Chapter
Pillars of Computer Science

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

  • 927 Accesses

Abstract

The symbolic method for verifying definite iterations over hierarchical data structures without loop invariants is extended to allow tuples of altered data structures and the termination statement which contains a condition depending on variables modified by the iteration body. Transformations of these generalized iterations to the standard ones are proposed and justified. A technique for generating verification conditions is described. The generalization of the symbolic verification method allows us to apply it to pointer programs. As a case study, programs over doubly-linked lists are considered. A program that merges in-place ordered doubly-linked lists is verified by the symbolic method without loop invariants.

This work was partly supported by Russian Foundation for Basic Research under grant 04-01-00114.

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. Abd-El-Hafiz, S.K., Basili, V.R.: A knowledge - based approach to the analysis of loops. IEEE Trans. of Software Eng. 22(5), 339–360 (1996)

    Article  Google Scholar 

  2. Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. Ernst, M.D., et al.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. of Software Eng. 27(2), 99–123 (2001)

    Article  Google Scholar 

  4. Gries, D., Gehani, N.: Some ideas on data types in high-level languages. Comm. ACM 20(6), 414–420 (1977)

    Article  MATH  Google Scholar 

  5. Hehner, E.C.R., Gravell, A.M.: Refinement semantics and  loop rules. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1497–1510. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Hoare, C.A.R.: An axiomatic basis of computer programming. Comm. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  7. Hoare, C.A.R.: A note on the for statement. BIT 12(3), 334–341 (1972)

    Article  MATH  Google Scholar 

  8. Hoare, C.A.R.: The verifying compiler: a grand challenge for computing research. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 1–12. Springer, Heidelberg (2004)

    Google Scholar 

  9. Immerman, N., et al.: Verification via structure si+mulation. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 281–294. Springer, Heidelberg (2004)

    Google Scholar 

  10. Linger, R.C., Mills, H.D., Witt, B.I.: Structured programming: theory and practice. Addison Wesley, Reading (1979)

    MATH  Google Scholar 

  11. Luckham, D.C., Suzuki, N.: Verification of array, record and pointer operations in Pascal. ACM Trans. on Programming Languages and Systems 1(2), 226–244 (1979)

    Article  MATH  Google Scholar 

  12. Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 121–135. Springer, Heidelberg (2003)

    Google Scholar 

  13. Meyer, B.: Towards practical proofs of class correctness. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 359–387. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  14. Mills, H.D.: Structured programming: retrospect and prospect. IEEE Software 3(6), 58–67 (1986)

    Article  Google Scholar 

  15. Morris, J.M.: A general axiom of assignment, Assignment and linked data structures. Lecture Notes of Intern. Summer School on Theoretical foundations of programming methodology, D. Reidel, pp. 25–41 (1982)

    Google Scholar 

  16. Necula, G.C.: Proof-carrying code. In: Proc. 24th Annual ACM Symposium on Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)

    Chapter  Google Scholar 

  17. Nepomniaschy, V.A.: Loop invariant elimination in program verification. Programming and Computer Software 3, 129–137 (1985) (English translation of Russian Journal ”Programmirovanie”)

    Google Scholar 

  18. Nepomniaschy, V.A.: On problem–oriented program verification. Programming and Computer Software 1, 1–9 (1986)

    Google Scholar 

  19. Nepomniaschy, V.A., Sulimov, A.A.: Problem-oriented means of program specification and verification in project SPECTRUM. In: Miola, A. (ed.) DISCO 1993. LNCS, vol. 722, pp. 374–378. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  20. Nepomniaschy, V.A., Sulimov, A.A.: Problem-oriented verification system and its application to linear algebra programs. Theoretical Computer Science 119, 173–185 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  21. Nepomniaschy, V.A.: Symbolic verification method for definite iteration over data structures. Information Processing Letters 69, 207–213 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  22. Nepomniaschy, V.A.: Verification of definite iteration over hierarchical data structures. In: Finance, J.-P. (ed.) ETAPS 1999 and FASE 1999. LNCS, vol. 1577, pp. 176–187. Springer, Heidelberg (1999)

    Google Scholar 

  23. Nepomniaschy, V.A.: Verification of definite iteration over tuples of data structures. Programming and Computer Software 1, 1–10 (2002)

    Article  Google Scholar 

  24. Nepomniaschy, V.A.: Symbolic verification method for definite iteration over altered data structures. Programming and Computer Software 1, 1–12 (2005)

    Google Scholar 

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

    Chapter  Google Scholar 

  26. Reynolds, J.C.: Reasoning about shared mutable data structure. In: Proc. Symp. in celebration of the work of C.A.R. Hoare, Oxford, pp. 1–22 (1999)

    Google Scholar 

  27. Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 271–288. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  28. Stavely, A.M.: Verifying definite iteration over data structures. IEEE Trans. of Software Eng. 21(6), 506–514 (1995)

    Article  Google Scholar 

  29. Whalen, M., Schumann, J., Fischer, B.: Synthesizing certified code. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 431–450. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Siberian Division, A.P. Ershov Institute of Informatics Systems, Russian Academy of Sciences, 6, Lavrentiev Ave., Novosibirsk, 630090, Russia

    Valery Nepomniaschy

Authors
  1. Valery Nepomniaschy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Arnon Avron Nachum Dershowitz Alexander Rabinovich

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Nepomniaschy, V. (2008). Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds) Pillars of Computer Science. Lecture Notes in Computer Science, vol 4800. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78127-1_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78127-1_29

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78126-4

  • Online ISBN: 978-3-540-78127-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation