{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:20Z","timestamp":1776305060019,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540213147","type":"print"},{"value":"9783540247326","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_18","type":"book-chapter","created":{"date-parts":[[2010,7,28]],"date-time":"2010-07-28T00:14:47Z","timestamp":1280276087000},"page":"252-266","source":"Crossref","is-referenced-by-count":32,"title":["Verifying Commit-Atomicity Using Model-Checking"],"prefix":"10.1007","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"7","key":"18_CR1","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/988376.988378","volume":"17","author":"M.P. Atkinson","year":"1981","unstructured":"Atkinson, M.P., Chisholm, K.J., Cockshott, W.P.: PS-Algol: an Algol with a persistent heap. ACM SIGPLAN Notices\u00a017(7), 24\u201331 (1981)","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"18_CR2","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1145\/4472.4477","volume":"7","author":"M.P. Atkinson","year":"1985","unstructured":"Atkinson, M.P., Morrison, D.: Procedures as persistent data objects. ACM Transactions on Programming Languages and Systems\u00a07(4), 539\u2013559 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/3-540-51285-3_42","volume-title":"PARLE \u201989 - Parallel Architectures and Languages Europe","author":"R.-J. Back","year":"1989","unstructured":"Back, R.-J.: A method for refining atomicity in parallel algorithms. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol.\u00a0366, pp. 199\u2013216. Springer, Heidelberg (1989)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"Proceedings of the International Conference on Concurrency Theory","author":"E. Cohen","year":"1998","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 317\u2013331. Springer, Heidelberg (1998)"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Deng, X., Dwyer, M., Hatcliff, J., Mizuno, M.: Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: International Conference on Software Engineering, pp. 442\u2013452 (2002)","DOI":"10.1145\/581392.581394"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Doeppner Jr., T.W.: Parallel program correctness through refinement. In: Proceedings of the ACM Symposium on the Principles of Programming Languages, pp. 155\u2013169 (1977)","DOI":"10.1145\/512950.512965"},{"key":"18_CR7","volume-title":"Camelot and Avalon: A Distributed Transaction Facility","author":"J.L. Eppinger","year":"1991","unstructured":"Eppinger, J.L., Mummert, L.B., Spector, A.Z.: Camelot and Avalon: A Distributed Transaction Facility. Morgan Kaufmann, San Francisco (1991)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: Proceedings of the ACM Symposium on the Principles of Programming Languages (2004)","DOI":"10.1145\/964001.964023"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, pp. 338\u2013349 (2003)","DOI":"10.1145\/781131.781169"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Types for atomicity. In: Proceedings of the ACM Workshop on Types in Language Design and Implementation, pp. 1\u201312 (2003)","DOI":"10.1145\/604174.604176"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. In: Workshop on Formal Techniques for Java-like Programs (2003)","DOI":"10.5381\/jot.2004.3.6.a4"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Harris, T.L., Fraser, K.: Language support for lightweight transactions. In: Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 388\u2013402 (2003)","DOI":"10.1145\/949305.949340"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Robby, Dwyer, M.B.: Verifying atomicity specifications for concurrent object-oriented software using model-checking. In: Proceedings of the International Conference on Verification, Model Checking and Abstract Interpretation (2004)","DOI":"10.1007\/978-3-540-24622-0_16"},{"issue":"3","key":"18_CR14","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Lamport, L., Schneider, F.B.: Pretending atomicity. Research Report 44, DEC Systems Research Center (1989)","DOI":"10.2307\/3562647"},{"issue":"12","key":"18_CR16","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Communications of the ACM\u00a018(12), 717\u2013721 (1975)","journal-title":"Communications of the ACM"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Liskov, B., Curtis, D., Johnson, P., Scheifler, R.: Implementation of Argus. In: Proceedings of the Symposium on Operating Systems Principles, pp. 111\u2013122 (1987)","DOI":"10.1145\/41457.37514"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Lomet, D.B.: Process structuring, synchronization, and recovery using atomic actions. Language Design for Reliable Software, 128\u2013137 (1977)","DOI":"10.1145\/800022.808319"},{"key":"18_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A Discipline of Multiprogramming: Programming Theory for Distributed Applications","author":"J. Misra","year":"2001","unstructured":"Misra, J.: A Discipline of Multiprogramming: Programming Theory for Distributed Applications. Springer, Heidelberg (2001)"},{"key":"18_CR20","volume-title":"The theory of database concurrency control","author":"C. Papadimitriou","year":"1986","unstructured":"Papadimitriou, C.: The theory of database concurrency control. Computer Science Press, Rockville (1986)"},{"key":"18_CR21","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. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 377\u2013390. Springer, Heidelberg (1994)"},{"key":"18_CR22","unstructured":"Qadeer, S., Wu, D.: Debugging concurrent programs with sequential analysis (2003) (submitted for publication)"},{"key":"18_CR23","series-title":"Electronic Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-39205-X","volume-title":"Proceedings of the Workshop on Runtime Verification","author":"L. Wang","year":"2003","unstructured":"Wang, L., Stoller, S.D.: Run-time analysis for atomicity. In: Proceedings of the Workshop on Runtime Verification. Electronic Notes in Computer Science, vol.\u00a089(2), Elsevier, Amsterdam (2003)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T11:06:30Z","timestamp":1685703990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}