{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:09:11Z","timestamp":1754482151172},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_16","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"175-190","source":"Crossref","is-referenced-by-count":49,"title":["Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking"],"prefix":"10.1007","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[]},{"family":"Robby","sequence":"additional","affiliation":[]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.: Bebop: a symbolic model-checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"16_CR2","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder \u2013 a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)"},{"key":"16_CR3","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"16_CR5","unstructured":"Dwyer, M.B., Hatcliff, J., Ranganath, V., Robby: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Technical Report TR2003-1, SAnToS Laboratory, Kansas State University (2003)"},{"issue":"11","key":"16_CR6","doi-asserted-by":"publisher","first-page":"1293","DOI":"10.1002\/(SICI)1096-9128(199711)9:11<1293::AID-CPE340>3.0.CO;2-J","volume":"9","author":"M.B. Dwyer","year":"1997","unstructured":"Dwyer, M.B., Wallentine, V.: A framework for parallel adaptive grid simulations. Concurrency: Practice and Experience\u00a09(11), 1293\u20131310 (1997)","journal-title":"Concurrency : Practice and Experience"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Type-based race detection for Java. In: PLDI (2000)","DOI":"10.1145\/349299.349328"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: Proceedings of POPL (2003) (to appear)","DOI":"10.1145\/964001.964023"},{"key":"16_CR9","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for sharedmemory programs. In: ESOP (2000)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI (2003)","DOI":"10.1145\/781131.781169"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"16_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall International, Englewood Cliffs (1991)"},{"issue":"5","key":"16_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013294 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Communications of the ACM\u00a018(12) (1975)","DOI":"10.1145\/361227.361234"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 377\u2013390. Springer, Heidelberg (1994)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)","DOI":"10.1145\/949952.940107"},{"key":"16_CR17","unstructured":"Bogor Website (2003), http:\/\/bogor.projects.cis.ksu.edu"},{"issue":"4","key":"16_CR18","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S. Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Transactions on Computer Systems"},{"key":"16_CR19","unstructured":"Stoller, S.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer, Springer (2002)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-36577-X_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Stoller","year":"2003","unstructured":"Stoller, S., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 489\u2013504. Springer, Heidelberg (2003)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Wang, L., Stoller, S.D.: Run-time analysis for atomicity. In: Proceedings of the Workshop on Runtime Verification. ENTCS, vol.\u00a089.2 (2003)","DOI":"10.1016\/S1571-0661(04)81049-1"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T17:40:50Z","timestamp":1559583650000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}