{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:28:39Z","timestamp":1770280119440,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540374060","type":"print"},{"value":"9783540374114","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_45","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"489-502","source":"Crossref","is-referenced-by-count":22,"title":["Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Burckhardt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milo M. K.","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"7","key":"45_CR1","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1095408.1095421","volume":"3","author":"H. Sutter","year":"2005","unstructured":"Sutter, H., Larus, J.: Software and the concurrency revolution. ACM Queue\u00a03(7), 54\u201362 (2005)","journal-title":"ACM Queue"},{"issue":"1","key":"45_CR2","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"M. Herlihy","year":"1991","unstructured":"Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst.\u00a013(1), 124\u2013149 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"45_CR3","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/357195.357198","volume":"5","author":"G.L. Peterson","year":"1983","unstructured":"Peterson, G.L.: Concurrent reading while writing. ACM Trans. Program. Lang. Syst.\u00a05(1), 46\u201355 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"11","key":"45_CR4","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1145\/359863.359878","volume":"20","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Concurrent reading and writing. Commun. ACM\u00a020(11), 806\u2013811 (1977)","journal-title":"Commun. ACM"},{"issue":"12","key":"45_CR5","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"issue":"9","key":"45_CR6","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp.\u00a0C-28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comp."},{"key":"45_CR7","doi-asserted-by":"crossref","unstructured":"Elmas, T., Tasiran, S., Qadeer, S.: VYRD: verifying concurrent programs by runtime refinement-violation detection. In: Programming Language Design and Implementation (PLDI), pp. 27\u201337 (2005)","DOI":"10.1145\/1065010.1065015"},{"key":"45_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"45_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-30482-1_11","volume-title":"Formal Methods and Software Engineering","author":"Y. Yang","year":"2004","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-model-sensitive data race analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 30\u201345. Springer, Heidelberg (2004)"},{"key":"45_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-540-27813-9_31","volume-title":"Computer Aided Verification","author":"G. Gopalakrishnan","year":"2004","unstructured":"Gopalakrishnan, G., Yang, Y., Sivaraj, H.: QB or not QB: An efficient execution verification tool for memory orderings. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 401\u2013413. Springer, Heidelberg (2004)"},{"key":"45_CR11","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Principles of Distributed Computing (PODC), pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"45_CR12","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: Principles and Practice of Parallel Programming (PPoPP), pp. 129\u2013136 (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"45_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"key":"45_CR14","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci.\u00a089(3) (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"},{"issue":"3","key":"45_CR15","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 Trans. Program. Lang. Syst.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"45_CR16","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: Symposium on Parallel Algorithms and Architectures (SPAA), pp. 34\u201341 (1995)","DOI":"10.1145\/215399.215413"},{"key":"45_CR17","first-page":"38","volume-title":"Symposium on Research on Integrated Systems","author":"D.L. Dill","year":"1993","unstructured":"Dill, D.L., Park, S., Nowatzyk, A.G.: Formal specification of abstract memory models. In: Symposium on Research on Integrated Systems, pp. 38\u201352. MIT Press, Cambridge (1993)"},{"issue":"4","key":"45_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 Trans. Comp. Sys.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comp. Sys."},{"key":"45_CR19","unstructured":"Frey, B.: PowerPC Architecture Book v2.02. International Business Machines Corporation (2005)"},{"key":"45_CR20","volume-title":"The SPARC Architecture Manual Version 9","year":"1994","unstructured":"Weaver, D.L., Germond, T. (eds.): The SPARC Architecture Manual Version 9. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"45_CR21","unstructured":"Compaq Computer Corporation. Alpha Architecture Reference Manual, 4th edn. (January 2002)"},{"key":"45_CR22","unstructured":"International Business Machines Corporation. z\/Architecture Principles of Operation, 1st edn. (December 2000)"},{"key":"45_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-39724-3_9","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yang","year":"2003","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Analyzing the Intel Itanium memory ordering rules using logic programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 81\u201395. Springer, Heidelberg (2003)"},{"key":"45_CR24","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: Logic in Computer Science (LICS), pp. 219\u2013228 (1996)","DOI":"10.1109\/LICS.1996.561322"},{"issue":"5","key":"45_CR25","doi-asserted-by":"publisher","first-page":"800","DOI":"10.1145\/1017460.1017464","volume":"51","author":"R.C. Steinke","year":"2004","unstructured":"Steinke, R.C., Nutt, G.J.: A unified theory of shared memory consistency. J. ACM\u00a051(5), 800\u2013849 (2004)","journal-title":"J. ACM"},{"key":"45_CR26","doi-asserted-by":"crossref","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: International Parallel and Distributed Processing Symposium (IPDPS) (2004)","DOI":"10.1109\/IPDPS.2004.1302944"},{"issue":"2","key":"45_CR27","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D. Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst.\u00a010(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"45_CR28","doi-asserted-by":"crossref","unstructured":"Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: International Conference on Supercomputing (ICS), pp. 285\u2013294 (2003)","DOI":"10.1145\/782814.782854"},{"key":"45_CR29","doi-asserted-by":"crossref","unstructured":"von Praun, C., Cain, T., Choi, J., Ryu, K.: Conditional memory ordering. In: International Symposium on Computer Architecture (ISCA) (2006)","DOI":"10.1109\/ISCA.2006.16"},{"key":"45_CR30","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference (DAC), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"45_CR31","doi-asserted-by":"crossref","unstructured":"Martin, M., Sorin, D., Cain, H., Hill, M., Lipasti, M.: Correctly implementing value prediction in microprocessors that support multithreading or multiprocessing. In: International Symposium on Microarchitecture (MICRO), pp. 328\u2013337 (2001)","DOI":"10.1109\/MICRO.2001.991130"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:16:01Z","timestamp":1605644161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11817963_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}