Advertisement

Automated Verification of Concurrent Linked Lists with Counters

  • Tuba Yavuz-Kahveci
  • Tevfik Bultan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

Abstract

We present an automated verification technique for verification of concurrent linked lists with integer variables. We show that using our technique one can automatically verify invariants that relate (unbounded) integer variables and heap variables such as head ≠ null → numItems > 0. The presented technique extends our previous work on composite symbolic representations with shape analysis. The main idea is to use different data structures such as BDDs, arithmetic constraints and shape graphs as type specific symbolic representations in automated verification. We show that polyhedra based widening operation can be integrated with summarization operation in shape graphs to conservatively verify properties of concurrent linked lists.

Keywords

Symbolic Representation Reachable State Transition Formula Shape Graph Presburger Arithmetic 
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. [AHH96]
    R. Alur, T. A. Henzinger, and P. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, March 1996.Google Scholar
  2. [BGP99]
    T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747–789, July 1999.Google Scholar
  3. [BYK01]
    T. Bultan and T. Yavuz-Kahveci. Action Language Verifier. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, 2001.Google Scholar
  4. [CC77]
    P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.Google Scholar
  5. [CH78]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th Annual ACM Symposium on Principles of Programming, pages 84–97, 1978.Google Scholar
  6. [CUD]
    CUDD: CU decision diagram package. http://vlsi.colorado.edu~fabio/CUDD/
  7. [CWZ90]
    D.R. Chase, M. Wegman, and F.K. Zadeck. Analysis of pointers and structures. In ACM SIGPLAN Conference on Program Language Design and Implementation, 1990.Google Scholar
  8. [Del00]
    G. Delzanno. Automatic verification of parameterized cache coherence protocols. In Proceedings of the 12th International Conference on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 53–68, 2000.CrossRefGoogle Scholar
  9. [DRS00]
    N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Jens Palsberg, editor, 7th International Static Analysis Symposium, Lecture Notes in Computer Science. Springer, 200.Google Scholar
  10. [HRP94]
    N. Halbwachs, P. Raymond, and Y. Proy. Verification of linear hybrid systems by means of convex approximations. In B. LeCharlier, editor, Proceedings of International Symposium on Static Analysis, volume 864 of Lecture Notes in Computer Science. Springer-Verlag, September 1994.Google Scholar
  11. [LARSW00]
    T. Lev-Ami, T. Reps, M. Sagiv, and R. Wilhelm. Putting static analysis to work for verification: A case study. In International Symposium on Software Testing And Analysis, 2000.Google Scholar
  12. [LAS00]
    T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analysis. In Jens Palsberg, editor, 7th International Static Analysis Symposium, Lecture Notes in Computer Science. Springer, 200.Google Scholar
  13. [Ome]
  14. [SRW98]
    M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. Transactions on Programming Languages and Systems, 20(1):1–50, 1998.CrossRefGoogle Scholar
  15. [Yah01]
    E. Yahav. Verifying safety properties of concurrent java programs using 3-valued logic. In ACM Symposium on Principles of Programming Languages, 2001.Google Scholar
  16. [YKB02]
    T. Yavuz-Kahveci and T. Bultan. Automated verification of concurrent linked lists with counters. Technical Report 2002-19, University of California, Santa Barbara, 2002.Google Scholar
  17. [YKTB01]
    T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. A library for composite symbolic representation. In Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Tuba Yavuz-Kahveci
    • 1
  • Tevfik Bultan
    • 1
  1. 1.Department of Computer ScienceUniversity of CaliforniaSanta BarbaraUSA

Personalised recommendations