Article

Automated Verification of Concurrent Linked Lists with Counters

Authors:

Tuba Yavuz-Kahveci,

Tevfik BultanAuthors Info & Claims

SAS '02: Proceedings of the 9th International Symposium on Static Analysis

Pages 69 - 84

Published: 17 September 2002 Publication History

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.

References

[1]

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.

[2]

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.

[3]

T. Bultan and T. Yavuz-Kahveci. Action Language Verifier. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering , 2001.

[4]

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.

[5]

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.

[6]

CUDD: CU decision diagram package. http://vlsi.colorado.edu/~fabio/CUDD/

[7]

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.

[8]

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.

[9]

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.

[10]

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.

[11]

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.

[12]

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.

[13]

The Omega project. http://www.cs.umd.edu/projects/omega/

[14]

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.

[15]

E. Yahav. Verifying safety properties of concurrent java programs using 3-valued logic. In ACM Symposium on Principles of Programming Languages , 2001.

[16]

T. Yavuz-Kahveci and T. Bultan. Automated verification of concurrent linked lists with counters. Technical Report 2002-19, University of California, Santa Barbara, 2002.

[17]

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.

Cited By

Roe KSmith STalpin JDerler PSchneider K(2017)Using the coq theorem prover to verify complex data structure invariantsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3127061(118-121)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3127061
Kidd NReps TDolby JVaziri M(2011)Finding concurrency-related bugs using random isolationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220897.322109513:6(495-518)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.5555/3220897.3221095
Gulwani SLev-Ami TSagiv M(2009)A combination framework for tracking partition sizesACM SIGPLAN Notices10.1145/1594834.148091244:1(239-251)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1594834.1480912
Show More Cited By

Automated Verification of Concurrent Linked Lists with Counters
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Specification and automated verification of concurrent software systems
Model checking unbounded concurrent lists

We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification ...
Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SAS '02: Proceedings of the 9th International Symposium on Static Analysis

September 2002

525 pages

ISBN:3540442359

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 September 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Roe KSmith STalpin JDerler PSchneider K(2017)Using the coq theorem prover to verify complex data structure invariantsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3127061(118-121)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3127061
Kidd NReps TDolby JVaziri M(2011)Finding concurrency-related bugs using random isolationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220897.322109513:6(495-518)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.5555/3220897.3221095
Gulwani SLev-Ami TSagiv M(2009)A combination framework for tracking partition sizesACM SIGPLAN Notices10.1145/1594834.148091244:1(239-251)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1594834.1480912
Gulwani SLev-Ami TSagiv MShao ZPierce B(2009)A combination framework for tracking partition sizesProceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1480881.1480912(239-251)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1480881.1480912
Magill SBerdine JClarke ECook B(2007)Arithmetic strengthening for shape analysisProceedings of the 14th international conference on Static Analysis10.5555/2391451.2391479(419-436)Online publication date: 22-Aug-2007
https://dl.acm.org/doi/10.5555/2391451.2391479
Gall TJeannet B(2007)Lattice automataProceedings of the 14th international conference on Static Analysis10.5555/2391451.2391457(52-68)Online publication date: 22-Aug-2007
https://dl.acm.org/doi/10.5555/2391451.2391457
Češka MErlebach PVojnar T(2006)Pattern-Based Verification of Programs with Extended Linear Linked Data StructuresElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.10.008145(113-130)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.1016/j.entcs.2005.10.008
Bouajjani AHabermehl PRogalewicz AVojnar T(2006)Abstract regular tree model checking of complex dynamic data structuresProceedings of the 13th international conference on Static Analysis10.1007/11823230_5(52-70)Online publication date: 29-Aug-2006
https://dl.acm.org/doi/10.1007/11823230_5
Balakrishnan GReps T(2006)Recency-Abstraction for heap-allocated storageProceedings of the 13th international conference on Static Analysis10.1007/11823230_15(221-239)Online publication date: 29-Aug-2006
https://dl.acm.org/doi/10.1007/11823230_15
Anand SPăsăreanu CVisser W(2006)Symbolic execution with abstract subsumption checkingProceedings of the 13th international conference on Model Checking Software10.1007/11691617_10(163-181)Online publication date: 30-Mar-2006
https://dl.acm.org/doi/10.1007/11691617_10
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten