{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T11:47:57Z","timestamp":1763466477935,"version":"3.41.0"},"reference-count":119,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2008,5,24]],"date-time":"2008-05-24T00:00:00Z","timestamp":1211587200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,5]]},"abstract":"<jats:p>We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are more precise than existing techniques. The framework also provides a precise shape-analysis algorithm for concurrent programs. In contrast to most existing verification techniques, we do not put a bound on the number of allocated objects. The framework produces interesting results even when analyzing programs with an unbounded number of threads. The framework is applied to successfully verify the following properties of a concurrent program:<\/jats:p>\n          <jats:p>\u2014Concurrent manipulation of linked-list based ADT preserves the ADT datatype invariant.<\/jats:p>\n          <jats:p>\u2014The program does not perform inconsistent updates due to interference.<\/jats:p>\n          <jats:p>\u2014The program does not reach a deadlock.<\/jats:p>\n          <jats:p>\u2014The program does not produce runtime errors due to illegal thread interactions.<\/jats:p>\n          <jats:p>We also found bugs in erroneous programs violating such properties. A prototype of our framework has been implemented and applied to small, but interesting, example programs.<\/jats:p>","DOI":"10.1145\/1745312.1745315","type":"journal-article","created":{"date-parts":[[2010,5,25]],"date-time":"2010-05-25T13:08:17Z","timestamp":1274792897000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying safety properties of concurrent heap-manipulating programs"],"prefix":"10.1145","volume":"32","author":[{"given":"Eran","family":"Yahav","sequence":"first","affiliation":[{"name":"IBM T. J. Watson Research Center, Hawthorne, NY"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel-Aviv University, Tel-Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,5,24]]},"reference":[{"volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99)","author":"Abdulla P. A.","key":"e_1_2_1_1_1","unstructured":"Abdulla , P. A. , Annichini , A. , Bensalem , S. , Bouajjani , A. , Habermehl , P. , and Lakhnech , Y . 1999. Verification of infinite-state systems by combining abstraction and reachability analysis . In Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99) . Springer-Verlag, Berlin, Germany, 146--159. Abdulla, P. A., Annichini, A., Bensalem, S., Bouajjani, A., Habermehl, P., and Lakhnech, Y. 1999. Verification of infinite-state systems by combining abstraction and reachability analysis. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99). Springer-Verlag, Berlin, Germany, 146--159."},{"volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","author":"Amit D.","key":"e_1_2_1_2_1","unstructured":"Amit , D. , Rinetzky , N. , Reps , T. , Sagiv , M. , and Yahav , E . 2007. Comparison under abstraction for verifying linearizability . In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07) . Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany. Amit, D., Rinetzky, N., Reps, T., Sagiv, M., and Yahav, E. 2007. Comparison under abstraction for verifying linearizability. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"volume-title":"Proceedings of the 5th NASA Langley Formal Methods Workshop (LFM'00)","author":"Bensalem S.","key":"e_1_2_1_6_1","unstructured":"Bensalem , S. , Ganesh , V. , Lakhnech , Y. , Mu\u00f1oz , C. , Owre , S. , Ruess , H. , Rushby , J. , Rusu , V. , Sa\u00efdi , H. , Shankar , N. , Singerman , E. , and Tiwari , A . 2000. An overview of SAL . In Proceedings of the 5th NASA Langley Formal Methods Workshop (LFM'00) , NASA, Hampton, VA, 187--196. Bensalem, S., Ganesh, V., Lakhnech, Y., Mu\u00f1oz, C., Owre, S., Ruess, H., Rushby, J., Rusu, V., Sa\u00efdi, H., Shankar, N., Singerman, E., and Tiwari, A. 2000. An overview of SAL. In Proceedings of the 5th NASA Langley Formal Methods Workshop (LFM'00), NASA, Hampton, VA, 187--196."},{"volume-title":"Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98)","author":"Bensalem S.","key":"e_1_2_1_7_1","unstructured":"Bensalem , S. , Lakhnech , Y. , and Owre , S . 1998. Invest: A tool for the verification of invariants . In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98) . Springer-Verlag, Berlin, Germany, 505--510. Bensalem, S., Lakhnech, Y., and Owre, S. 1998. Invest: A tool for the verification of invariants. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98). Springer-Verlag, Berlin, Germany, 505--510."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science","volume":"4590","author":"Berdine J.","unstructured":"Berdine , J. , Calcagno , C. , Cook , B. , Distefano , D. , O Hearn , P. W. , Wies , T. , and Yang , H . 2007. Shape analysis for composite data structures . In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science , vol. 4590 . Springer-Verlag, Berlin, Germany, 178--192. Berdine, J., Calcagno, C., Cook, B., Distefano, D., OHearn, P. W., Wies, T., and Yang, H. 2007. Shape analysis for composite data structures. In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 178--192."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","volume":"4590","author":"Bogudlov I.","unstructured":"Bogudlov , I. , Lev-Ami , T. , Reps , T. W. , and Sagiv , M . 2007. Revamping TVLA: Making parametric shape analysis competitive . In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07) . Lecture Notes in Computer Science , vol. 4590 . Springer-Verlag, Berlin, Germany, 221--225. Bogudlov, I., Lev-Ami, T., Reps, T. W., and Sagiv, M. 2007. Revamping TVLA: Making parametric shape analysis competitive. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 221--225."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582440"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504287"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/214037.214100"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS'98)","volume":"1378","author":"Cardelli L.","unstructured":"Cardelli , L. and Gordon , A. D . 1998. Mobile ambients . In Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS'98) . Lecture Notes in Computer Science , vol. 1378 . Springer-Verlag, Berlin, Germany, 140--155. Cardelli, L. and Gordon, A. D. 1998. Mobile ambients. In Proceedings of the Foundations of Software Science and Computation Structures (FoSSaCS'98). Lecture Notes in Computer Science, vol. 1378. Springer-Verlag, Berlin, Germany, 140--155."},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Cenciarelli P. Knapp A. Reus B. and Wirsing M. 1999. An event-based structural operational semantis of multi-threaded Java. In Formal Syntax and Semantics of Java. Springer-Verlag Berlin Germany 157--200.   Cenciarelli P. Knapp A. Reus B. and Wirsing M. 1999. An event-based structural operational semantis of multi-threaded Java. In Formal Syntax and Semantics of Java. Springer-Verlag Berlin Germany 157--200.","DOI":"10.1007\/3-540-48737-9_5"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93585"},{"key":"e_1_2_1_20_1","unstructured":"Choi J. Loginov A. and Sarkar V. 2001. Static datarace analysis for multithreaded object-oriented programs. IBM Research Report 22146 IBM Research.  Choi J. Loginov A. and Sarkar V. 2001. Static datarace analysis for multithreaded object-oriented programs. IBM Research Report 22146 IBM Research."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_22_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999a. Model Checking. MIT Press Cambridge MA.   Clarke E. Grumberg O. and Peled D. 1999a. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems","author":"Clarke E.","unstructured":"Clarke , E. , Talupur , M. , and H. V. 2008. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems . In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science , vol. 4963 . Springer-Verlag , Berlin, Germany , 33--47. Clarke, E., Talupur, M., and H. V. 2008. Proving ptolemy right: The environment abstraction framework for model checking concurrent systems. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 33--47."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_9"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/265943.265960"},{"key":"e_1_2_1_26_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999b. Model Checking. MIT Press Cambridge MA.   Clarke E. M. Grumberg O. and Peled D. A. 1999b. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_9"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/332740.332741"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"volume-title":"Proceedings of the 11th International Conference on Computer-Aided Verification. Springer-Verlag","author":"Das S.","key":"e_1_2_1_33_1","unstructured":"Das , S. , Dill , D. , and Park , S . 1999. Experience with predicate abstraction . In Proceedings of the 11th International Conference on Computer-Aided Verification. Springer-Verlag , Berlin, Germany. Das, S., Dill, D., and Park, S. 1999. Experience with predicate abstraction. In Proceedings of the 11th International Conference on Computer-Aided Verification. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199906)29:7%3C577::AID-SPE246%3E3.0.CO;2-V"},{"volume-title":"Proceedings of the 5th and 6th International SPIN Wokshops on Theoretical and Practical Aspects of SPIN Model Checking. Springer-Verlag","author":"Demartini C.","key":"e_1_2_1_35_1","unstructured":"Demartini , C. , Iosif , R. , and Sisto , R . 1999b. dSPIN: A dynamic extension of SPIN . In Proceedings of the 5th and 6th International SPIN Wokshops on Theoretical and Practical Aspects of SPIN Model Checking. Springer-Verlag , Berlin, Germany, 261--276. Demartini, C., Iosif, R., and Sisto, R. 1999b. dSPIN: A dynamic extension of SPIN. In Proceedings of the 5th and 6th International SPIN Wokshops on Theoretical and Practical Aspects of SPIN Model Checking. Springer-Verlag, Berlin, Germany, 261--276."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the International Conference in Computer-Aided Verification (CAV). Lecture Notes in Computer Science","volume":"697","author":"Emerson E. A.","unstructured":"Emerson , E. A. and Sistla , A. P . 1993. Symmetry and model checking . In Proceedings of the International Conference in Computer-Aided Verification (CAV). Lecture Notes in Computer Science , vol. 697 . Springer-Verlag, Berlin, Germany, 463--478. Emerson, E. A. and Sistla, A. P. 1993. Symmetry and model checking. In Proceedings of the International Conference in Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 697. Springer-Verlag, Berlin, Germany, 463--478."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945468"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the International Conference in Computer-Aided Verification (CAV'04)","volume":"3114","author":"Farzan A.","unstructured":"Farzan , A. , Chen , F. , Meseguer , J. , and Rosu , G . 2004. Formal analysis of java programs in javafan . In Proceedings of the International Conference in Computer-Aided Verification (CAV'04) . Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag, Berlin, Germany, 501--505. Farzan, A., Chen, F., Meseguer, J., and Rosu, G. 2004. Formal analysis of java programs in javafan. In Proceedings of the International Conference in Computer-Aided Verification (CAV'04). Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 501--505."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146254"},{"volume-title":"Proceedings of the 8th European Symposium on Programming Languages and Systems (ESOP'99)","author":"Flanagan C.","key":"e_1_2_1_41_1","unstructured":"Flanagan , C. and Abadi , M . 1999. Types for safe locking . In Proceedings of the 8th European Symposium on Programming Languages and Systems (ESOP'99) . Springer-Verlag, Berlin, Germany, 91--108. Flanagan, C. and Abadi, M. 1999. Types for safe locking. In Proceedings of the 8th European Symposium on Programming Languages and Systems (ESOP'99). Springer-Verlag, Berlin, Germany, 91--108."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 11th Annual International Symposium on Static Analysis (SAS'04)","volume":"3148","author":"Flanagan C.","unstructured":"Flanagan , C. and Freund , S. N . 2004. Type inference against races . In Proceedings of the 11th Annual International Symposium on Static Analysis (SAS'04) . Lecture Notes in Computer Science , vol. 3148 . Springer-Verlag, Berlin, Germany, 116--132. Flanagan, C. and Freund, S. N. 2004. Type inference against races. In Proceedings of the 11th Annual International Symposium on Static Analysis (SAS'04). Lecture Notes in Computer Science, vol. 3148. Springer-Verlag, Berlin, Germany, 116--132."},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the 11th European Symposium on Programming (ESOP'02)","volume":"2305","author":"Flanagan C.","unstructured":"Flanagan , C. , Freund , S. N. , and Qadeer , S . 2002. Thread-modular verification for shared-memory programs . In Proceedings of the 11th European Symposium on Programming (ESOP'02) . Lecture Notes in Computer Science , vol. 2305 . Springer-Verlag, Berlin, Germany, 262--277. Flanagan, C., Freund, S. N., and Qadeer, S. 2002. Thread-modular verification for shared-memory programs. In Proceedings of the 11th European Symposium on Programming (ESOP'02). Lecture Notes in Computer Science, vol. 2305. Springer-Verlag, Berlin, Germany, 262--277."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375618"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_10"},{"key":"e_1_2_1_48_1","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem","author":"Godefroid P.","unstructured":"Godefroid , P. 1996. Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem . Lecture Notes in Computer Science , vol. 1032 . Springer-Verlag , Berlin, Germany . Godefroid, P. 1996. Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem. Lecture Notes in Computer Science, vol. 1032. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_49_1","unstructured":"Goetz B. Peierls T. Bloch J. Bowbeer J. Holmes D. and Lea D. 2006. Java Concurrency in Practice. Addison-Wesley Reading MA.   Goetz B. Peierls T. Bloch J. Bowbeer J. Holmes D. and Lea D. 2006. Java Concurrency in Practice. Addison-Wesley Reading MA."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040333"},{"key":"e_1_2_1_51_1","unstructured":"Gosling J. Joy B. and Steele G. 1997. The Java Language Specification. The Java Series. Addison-Wesley Reading MA.   Gosling J. Joy B. and Steele G. 1997. The Java Language Specification. The Java Series. Addison-Wesley Reading MA."},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS'07)","volume":"4807","author":"Gotsman A.","unstructured":"Gotsman , A. , Berdine , J. , Cook , B. , Rinetzky , N. , and Sagiv , M . 2007a. Local reasoning for storable locks and threads . In Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS'07) . Lecture Notes in Computer Science , vol. 4807 . Springer-Verlag, Berlin, Germany, 19--37. Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., and Sagiv, M. 2007a. Local reasoning for storable locks and threads. In Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS'07). Lecture Notes in Computer Science, vol. 4807. Springer-Verlag, Berlin, Germany, 19--37."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250765"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480886"},{"key":"e_1_2_1_55_1","volume-title":"Lecture Notes in Computer Science","volume":"1254","author":"Graf S.","unstructured":"Graf , S. and Saidi , H . 1997. Construction of abstract state graphs with PVS . Lecture Notes in Computer Science , vol. 1254 , Springer-Verlag, Berlin, Germany, 72--83. Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. Lecture Notes in Computer Science, vol. 1254, Springer-Verlag, Berlin, Germany, 72--83."},{"key":"e_1_2_1_56_1","volume-title":"Technical Report TA-CS-2006-052, School of Computer Science, Tel-Aviv, Univ. Tel-Aviv, Israel. (Avialable at \u201chttp:\/\/www.cs.tau.ac.il\/~msagiv\/skipping.ps\u201d.)","author":"Gueta G.","year":"2006","unstructured":"Gueta , G. , Flanagan , C. , Yahav , E. , and Sagiv , M . 2006 . A semantics for reducing nondeterminism in concurrent programs and its applications. Technical Report TA-CS-2006-052, School of Computer Science, Tel-Aviv, Univ. Tel-Aviv, Israel. (Avialable at \u201chttp:\/\/www.cs.tau.ac.il\/~msagiv\/skipping.ps\u201d.) Gueta, G., Flanagan, C., Yahav, E., and Sagiv, M. 2006. A semantics for reducing nondeterminism in concurrent programs and its applications. Technical Report TA-CS-2006-052, School of Computer Science, Tel-Aviv, Univ. Tel-Aviv, Israel. (Avialable at \u201chttp:\/\/www.cs.tau.ac.il\/~msagiv\/skipping.ps\u201d.)"},{"volume-title":"Proceedings of the 14th Workshop on Model Checking Software (SPIN'07)","author":"Gueta G.","key":"e_1_2_1_57_1","unstructured":"Gueta , G. , Flanagan , C. , Yahav , E. , and Sagiv , M . 2007. Cartesian partial order reduction . In Proceedings of the 14th Workshop on Model Checking Software (SPIN'07) . Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany. Gueta, G., Flanagan, C., Yahav, E., and Sagiv, M. 2007. Cartesian partial order reduction. In Proceedings of the 14th Workshop on Model Checking Software (SPIN'07). Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996844"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_2_1_61_1","unstructured":"Herlihy M. and Shavit N. 2008. The Art of Multiprocessor Programming. Morgan-Kaufmann San Francisco CA.   Herlihy M. and Shavit N. 2008. The Art of Multiprocessor Programming. Morgan-Kaufmann San Francisco CA."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.5555\/646730.703666"},{"key":"e_1_2_1_64_1","unstructured":"IBM. 1983. IBM System\/370 Extended Architecture Principles of Operation. Publication No. SA22-7085.  IBM. 1983. IBM System\/370 Extended Architecture Principles of Operation. Publication No. SA22-7085."},{"volume-title":"Texts in Computer Science","author":"Immerman N.","key":"e_1_2_1_65_1","unstructured":"Immerman , N. 1998. Descriptive Complexity . Texts in Computer Science . Springer-Verlag , Berlin, Germany . Immerman, N. 1998. Descriptive Complexity. Texts in Computer Science. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_67_1","volume-title":"Proceedings of the 11th International Symposium on Static Analysis, (SAS'04)","volume":"3148","author":"Jeannet B.","unstructured":"Jeannet , B. , Loginov , A. , Reps , T. W. , and Sagiv , S . 2004. A relational approach to interprocedural shape analysis . In Proceedings of the 11th International Symposium on Static Analysis, (SAS'04) . Lecture Notes in Computer Science , vol. 3148 . Springer-Verlag, Berlin, Germany, 246--264. Jeannet, B., Loginov, A., Reps, T. W., and Sagiv, S. 2004. A relational approach to interprocedural shape analysis. In Proceedings of the 11th International Symposium on Static Analysis, (SAS'04). Lecture Notes in Computer Science, vol. 3148. Springer-Verlag, Berlin, Germany, 246--264."},{"key":"e_1_2_1_68_1","first-page":"102","article-title":"Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, NJ","volume":"4","author":"Jones N.","year":"1981","unstructured":"Jones , N. and Muchnick , S. 1981 . Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, NJ , Chapter 4 , 102 -- 131 . Jones, N. and Muchnick, S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, NJ, Chapter 4, 102--131.","journal-title":"Chapter"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582161"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_38"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_7"},{"volume-title":"Concurrent Programming in Java","author":"Lea D.","key":"e_1_2_1_73_1","unstructured":"Lea , D. 1997. Concurrent Programming in Java . Addison-Wesley, Reading , MA. Lea, D. 1997. Concurrent Programming in Java. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_1_75_1","series-title":"Lecture Notes in Computer Science","volume-title":"TVLA: A framework for Kleene based static analysis. In Proceedings of the Static Analysis Symposium","author":"Lev-Ami T.","year":"2000","unstructured":"Lev-Ami , T. , and Sagiv , M . 2000 . TVLA: A framework for Kleene based static analysis. In Proceedings of the Static Analysis Symposium . Lecture Notes in Computer Science , vol. 1824 . Springer-Verlag , Berlin, Germany , 280--301. Lev-Ami, T., and Sagiv, M. 2000. TVLA: A framework for Kleene based static analysis. In Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 1824. Springer-Verlag, Berlin, Germany, 280--301."},{"key":"e_1_2_1_76_1","unstructured":"Lindholm T. and Yellin F. 1997. The Java Virtual Machine Specification. The Java Series. Addison-Wesley Reading MA.   Lindholm T. and Yellin F. 1997. The Java Virtual Machine Specification. The Java Series. Addison-Wesley Reading MA."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_24"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_13"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514189"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/130616.130623"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651923"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02)","author":"Pnueli A.","key":"e_1_2_1_87_1","unstructured":"Pnueli , A. , Xu , J. , and Zuck , L. D . 2002. Liveness with (0, 1, infty)-counter abstraction . In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02) . Springer-Verlag, Berlin, Germany, 107--122. Pnueli, A., Xu, J., and Zuck, L. D. 2002. Liveness with (0, 1, infty)-counter abstraction. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02). Springer-Verlag, Berlin, Germany, 107--122."},{"volume-title":"Proceedings of the International Conference on Parallel Processing. CRC Press, 68--75","author":"Prakash S.","key":"e_1_2_1_88_1","unstructured":"Prakash , S. , Lee , Y. , and Johnson , T . 1991. A non-blocking algorithm for shared queues using Compare-and-Swap . In Proceedings of the International Conference on Parallel Processing. CRC Press, 68--75 . Prakash, S., Lee, Y., and Johnson, T. 1991. A non-blocking algorithm for shared queues using Compare-and-Swap. In Proceedings of the International Conference on Parallel Processing. CRC Press, 68--75."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134019"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_91_1","volume-title":"Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science","volume":"2618","author":"Reps T.","unstructured":"Reps , T. , Sagiv , M. , and Loginov , A . 2003. Finite differencing of logical formulas for static analysis . In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science , vol. 2618 . Springer-Verlag, Berlin, Germany. Reps, T., Sagiv, M., and Loginov, A. 2003. Finite differencing of logical formulas for static analysis. In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 2618. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_92_1","volume-title":"Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science","volume":"3114","author":"Reps T. W.","unstructured":"Reps , T. W. , Sagiv , M. , and Wilhelm , R . 2004. Static program analysis via 3-valued logic . In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science , vol. 3114 . Springer-Verlag, Berlin, Germany, 401--404. Reps, T. W., Sagiv, M., and Wilhelm, R. 2004. Static program analysis via 3-valued logic. In Proceedings of the Computer Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, Berlin, Germany, 401--404."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_94_1","doi-asserted-by":"crossref","unstructured":"Rinetskey N.\n     and \n      Sagiv M\n  . \n  2001\n  . Interprocedural shape analysis for recursive programs. In Proceedings of the International Conference on Compiler Construction Lecture Notes in Computer Science vol. \n  2027\n  . \n  Springer-Verlag Berlin Germany 133--149.   Rinetskey N. and Sagiv M. 2001. Interprocedural shape analysis for recursive programs. In Proceedings of the International Conference on Compiler Construction Lecture Notes in Computer Science vol. 2027. Springer-Verlag Berlin Germany 133--149.","DOI":"10.1007\/3-540-45306-7_10"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.5555\/647169.760067"},{"key":"e_1_2_1_99_1","volume-title":"Proceedings of the 10th International Static Analysis Symposium (SAS'03)","volume":"2694","author":"Shaham R.","unstructured":"Shaham , R. , Yahav , E. , Kolodner , E. K. , and Sagiv , M . 2003. Establishing local temporal heap safety properties with applications to compile-time memory management . In Proceedings of the 10th International Static Analysis Symposium (SAS'03) . Lecture Notes in Computer Science , vol. 2694 . Springer-Verlag, Berlin, Germany. Shaham, R., Yahav, E., Kolodner, E. K., and Sagiv, M. 2003. Establishing local temporal heap safety properties with applications to compile-time memory management. In Proceedings of the 10th International Static Analysis Symposium (SAS'03). Lecture Notes in Computer Science, vol. 2694. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_100_1","unstructured":"Silberschatz A. and Galvin P. B. 1994. Operating Systems Concepts 4 Ed. Addison-Wesley Reading MA.   Silberschatz A. and Galvin P. B. 1994. Operating Systems Concepts 4 Ed. Addison-Wesley Reading MA."},{"key":"e_1_2_1_101_1","volume-title":"USENIX Technical Conference Proceedings. ACM","author":"Sterling N.","year":"1993","unstructured":"Sterling , N. 1993 . Warlock\u2014A static data race analysis tool . In USENIX Technical Conference Proceedings. ACM , New York, 97--106. Sterling, N. 1993. Warlock\u2014A static data race analysis tool. In USENIX Technical Conference Proceedings. ACM, New York, 97--106."},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672084"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.5555\/110382.110466"},{"key":"e_1_2_1_104_1","volume-title":"Proceedings of the Parallel and Distributed Computing in Engineering Systems. Elsevier Science Publishers","author":"Stone J. M.","year":"1992","unstructured":"Stone , J. M. 1992 . A non-blocking Compare-and-Swap algorithm for a shared circular queue . In Proceedings of the Parallel and Distributed Computing in Engineering Systems. Elsevier Science Publishers , Amsterdam, The Netherlands, 147--152. Stone, J. M. 1992. A non-blocking Compare-and-Swap algorithm for a shared circular queue. In Proceedings of the Parallel and Distributed Computing in Engineering Systems. Elsevier Science Publishers, Amsterdam, The Netherlands, 147--152."},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567093"},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_27"},{"volume-title":"Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collabrative Research. IBM, 125--135","author":"Vall\u00e9e-Rai R.","key":"e_1_2_1_109_1","unstructured":"Vall\u00e9e-Rai , R. , Hendren , L. , Sundaresan , V. , Lam , P. , Gagnon , E. , and Co , P . 1999. Soot - A java optimization framework . In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collabrative Research. IBM, 125--135 . Vall\u00e9e-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., and Co, P. 1999. Soot - A java optimization framework. In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collabrative Research. IBM, 125--135."},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.5555\/111948.111969"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375598"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250787"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"e_1_2_1_114_1","article-title":"Java deadlock: The woes of multithreaded design","volume":"22","author":"Vermeulen A.","year":"1997","unstructured":"Vermeulen , A. 1997 . Java deadlock: The woes of multithreaded design . Dr. Dobb's J. Softw. Tools 22 , 9, 52, 54--56, 88, 89. Vermeulen, A. 1997. Java deadlock: The woes of multithreaded design. Dr. Dobb's J. Softw. Tools 22, 9, 52, 54--56, 88, 89.","journal-title":"Dr. Dobb's J. Softw. Tools"},{"key":"e_1_2_1_115_1","unstructured":"Wing J. M. and Gong C. 1990. A library of concurrent objects and their proofs of correctness. Tech. rep. CMU--CS--90--151 CMU.  Wing J. M. and Gong C. 1990. A library of concurrent objects and their proofs of correctness. Tech. rep. CMU--CS--90--151 CMU."},{"key":"e_1_2_1_116_1","unstructured":"Yahav E. 2000. 3VMC user's manual. Available at http:\/\/www.math.tau.ac.il\/~yahave.  Yahav E. 2000. 3VMC user's manual. Available at http:\/\/www.math.tau.ac.il\/~yahave."},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"},{"key":"e_1_2_1_118_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996846"},{"key":"e_1_2_1_119_1","volume-title":"Electronic Notes in Theoretical Computer Science","volume":"89","author":"Yahav E.","unstructured":"Yahav , E. , and Sagiv , M . 2003. Automatically verifying concurrent queue algorithms . Electronic Notes in Theoretical Computer Science , vol. 89 . Elsevier, Amsterdam, The Netherlands. Yahav, E., and Sagiv, M. 2003. Automatically verifying concurrent queue algorithms. Electronic Notes in Theoretical Computer Science, vol. 89. Elsevier, Amsterdam, The Netherlands."},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1745312.1745315","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1745312.1745315","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:16Z","timestamp":1750278376000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1745312.1745315"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,24]]},"references-count":119,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1145\/1745312.1745315"],"URL":"https:\/\/doi.org\/10.1145\/1745312.1745315","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2008,5,24]]},"assertion":[{"value":"2007-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-05-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}