{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:27:39Z","timestamp":1725488859804},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442356"},{"type":"electronic","value":"9783540457893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45789-5_8","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T09:50:10Z","timestamp":1186825810000},"page":"69-84","source":"Crossref","is-referenced-by-count":16,"title":["Automated Verification of Concurrent Linked Lists with Counters"],"prefix":"10.1007","author":[{"given":"Tuba","family":"Yavuz-Kahveci","sequence":"first","affiliation":[]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,5]]},"reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"R. Alur, T. A. Henzinger, and P. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181\u2013201, March 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"8_CR2","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"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\u2013789, July 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"T. Bultan and T. Yavuz-Kahveci. Action Language Verifier. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, 2001.","DOI":"10.1109\/ASE.2001.989834"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"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\u201397, 1978.","DOI":"10.1145\/512760.512770"},{"key":"8_CR6","unstructured":"CUDD: CU decision diagram package. \n                  http:\/\/vlsi.colorado.edu~fabio\/CUDD\/"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/93542.93585"},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"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\u201368, 2000."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-540-45099-3_7"},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of International Symposium on Static Analysis","author":"N. Halbwachs","year":"1994","unstructured":"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."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/347324.348031"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"8_CR13","unstructured":"The Omega project. \n                  http:\/\/www.cs.umd.edu\/projects\/omega\/"},{"issue":"1","key":"8_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"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\u201350, 1998.","journal-title":"Transactions on Programming Languages and Systems"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"E. Yahav. Verifying safety properties of concurrent java programs using 3-valued logic. In ACM Symposium on Principles of Programming Languages, 2001.","DOI":"10.1145\/360204.360206"},{"key":"8_CR16","volume-title":"Technical Report 2002-19","author":"T. Yavuz-Kahveci","year":"2002","unstructured":"T. Yavuz-Kahveci and T. Bultan. Automated verification of concurrent linked lists with counters. Technical Report 2002-19, University of California, Santa Barbara, 2002."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-45319-9_5"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45789-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T05:25:25Z","timestamp":1550726725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45789-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442356","9783540457893"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45789-5_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}