{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T16:30:49Z","timestamp":1775838649591,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540223429","type":"print"},{"value":"9783540278139","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_33","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T00:57:57Z","timestamp":1284425877000},"page":"427-439","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values"],"prefix":"10.1007","author":[{"given":"Jesse","family":"Bingham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anne","family":"Condon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhichuan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"33_CR1","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1145\/151646.151651","volume":"15","author":"Y. Afek","year":"1993","unstructured":"Afek, Y., Brown, G., Merritt, M.: Lazy caching. ACM Trans. on Prog. Lang. and Sys.\u00a015(1), 182\u2013205 (1993)","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K.L., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: 11th IEEE Symp. on Logic in Comp. Sci. pp. 219\u2013229 (1996)","DOI":"10.1109\/LICS.1996.561322"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-44585-4_42","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T.: Using timestamping and history variables to verify sequential consistency. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 423\u2013435. Springer, Heidelberg (2001)"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Barroso, L.A., Gharachorloo, K., McNamara, R., Nowatzyk, A., Qadeer, S., Sano, B., Smith, S., Stets, R., Verghese, B.: Piranha: a scalable architecture based on single-chip multiprocessing. In: 27th Int\u2019l. Symp. on Comp. Arch. pp. 282\u2013293 (2000)","DOI":"10.1145\/339647.339696"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Bilir, E.E., Dickson, R.M., Hu, Y., Plakal, M., Sorin, D.J., Hill, M.D., Wood, D.A.: Multicast snooping: a new coherence method using a multicast address network. In: 26th Int\u2019l. Symp. on Comp. Arch. pp. 294\u2013304 (1999)","DOI":"10.1145\/307338.301004"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Bingham, J.D., Condon, A., Hu, A.J.: Toward a decidable notion of sequential consistency. In: 15th ACM Symp. on Parallel Algorithms and Architectures (SPAA 2003), pp. 304\u2013313 (2003)","DOI":"10.1145\/777412.777467"},{"key":"33_CR8","unstructured":"Braun, T., Condon, A., Hu, A.J., Juse, K.S., Laza, M., Leslie, M., Sharma, R.: Proving sequential consistency by model checking. In: IEEE Int\u2019l. High Level Design Validation and Test Workshop (HLDVT), pp. 103\u2013108,;An expanded version appeared as University of British Columbia Dept. of Computer Science Tech Report TR-2001-03 (2001), http:\/\/www.cs.ubc.ca\/cgibin\/tr\/2001\/TR-2001-03"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Condon, A., Hu, A.J.: Automatable verification of sequential consistency. In: 13th ACM Symp. on Parallel Algorithms and Architectures (SPAA 2001), pp. 113\u2013121 (2001)","DOI":"10.1145\/378580.378604"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Symp. on Princ. of Prog. Lang., pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Gopalakrishnan, G., Ghughal, R., Hosabettu, R., Mokkedem, A., Nalumasu, R.: Formal modeling and validation applied to a commercial coherent bus: a case study. In: Conf on Correct Hardware Design and Verification Methods (CHARME), pp. 48\u201362 (1997)","DOI":"10.1007\/978-0-387-35190-2_4"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48683-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1999","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Verifying sequential consistency on sharedmemory multiprocessor systems. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 301\u2013315. Springer, Heidelberg (1999)"},{"issue":"3","key":"33_CR16","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M. Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.: Linearizability: a correctness condition for concurrent objects. ACM Trans. on Prog. Lang. and Sys.\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"33_CR17","doi-asserted-by":"crossref","unstructured":"Hill, M.D.: Multiprocessors should support simple memory-consistency models. IEEE Computer, 28\u201334 (August 1998)","DOI":"10.1109\/2.707614"},{"key":"33_CR18","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Int\u2019l. Conf. on Computer Hardware Description Languages, pp. 87\u2013100 (1993)"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Kuskin, J., Ofelt, D., Heinrich, M., Heinlein, J., Simoni, R., Gharachorloo, K., Chapin, J., Nakahira, D., Baxter, J., Horowitz, M., Gupta, A., Rosenblum, M., Hennessy, J.: The Stanford FLASH multiprocessor. In: 21st Int\u2019l. Symp. on Comp. Arch., pp. 302\u2013313 (1994)","DOI":"10.1109\/ISCA.1994.288140"},{"issue":"9","key":"33_CR20","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. on Computers\u00a0C-28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. on Computers"},{"issue":"4","key":"33_CR21","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/BF00709156","volume":"1","author":"P. Loewenstein","year":"1992","unstructured":"Loewenstein, P., Dill, D.L.: Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. Formal Methods in System Design\u00a01(4), 355\u2013383 (1992)","journal-title":"Formal Methods in System Design"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Martin, M.M.K., Hill, M.D., Wood, D.A.: Token coherence: low-latency coherence on unordered interconnects. In: Int\u2019l. Symp. on Comp. Arch., pp. 182\u2013193 (2003)","DOI":"10.1145\/859618.859640"},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 179\u2013195. Springer, Heidelberg (2001)"},{"key":"#cr-split#-33_CR24.1","doi-asserted-by":"crossref","unstructured":"Merritt, M. (ed.): Distributed Computing, 12(2-3) (1999);","DOI":"10.1007\/s004460050056"},{"key":"#cr-split#-33_CR24.2","unstructured":"Special issue devoted to proving sequential consistency of lazy caching"},{"key":"33_CR25","unstructured":"Nalumasu, R.: Formal Design and Verification Methods for Shared Memory Systems. PhD thesis, University of Utah (1999)"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.: Verification of the FLASH cache coherence protocol by aggregation of distributed transactions. In: 8th Symp. on Parallel Algorithms and Architectures, pp. 288\u2013296 (1996)","DOI":"10.1145\/237502.237573"},{"key":"33_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"issue":"1","key":"33_CR28","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F. Pong","year":"1997","unstructured":"Pong, F., Dubois, M.: Verification techniques for cache coherence protocols. ACM Computing Surveys\u00a029(1), 82\u2013126 (1997)","journal-title":"ACM Computing Surveys"},{"issue":"8","key":"33_CR29","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1109\/TPDS.2003.1225053","volume":"14","author":"S. Qadeer","year":"2003","unstructured":"Qadeer, S.: Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans. on Parallel and Distributed Systems\u00a014(8), 730\u2013741 (2003); Also appeared as Compaq Systems Research Center Report 176 (December 2001)","journal-title":"IEEE Trans. on Parallel and Distributed Systems"},{"key":"33_CR30","unstructured":"Scheurich, C.: Access Ordering and Coherence in Shared Memory Multiprocessors. PhD thesis, University of Southern California, USC Tech Report CENG 89-19 (May 1989)"},{"key":"33_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-60385-9_13","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 206\u2013224. Springer, Heidelberg (1995)"},{"key":"33_CR32","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: 13th Symp. on Princ. of Prog. Lang., pp. 184\u2013192 (1986)","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:22:05Z","timestamp":1605741725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}