{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:18:22Z","timestamp":1778077102540,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_26","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"273-287","source":"Crossref","is-referenced-by-count":52,"title":["Generating Litmus Tests for Contrasting Memory Consistency Models"],"prefix":"10.1007","author":[{"given":"Sela","family":"Mador-Haim","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]},{"given":"Milo M. K.","family":"Martin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","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. IEEE Computer\u00a029, 66\u201376 (1996)","journal-title":"IEEE Computer"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: DAMP (2009)","DOI":"10.1145\/1629635.1629638"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI, pp. 68\u201378 (2008)","DOI":"10.1145\/1379022.1375591"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321 (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"key":"26_CR6","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. Technical Report MSR-TR-2008-12, Microsoft Research (2008)"},{"key":"26_CR7","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency in relaxed memory models. Technical Report UCB\/EECS-2010-31, EECS Department, University of California, Berkeley (March 2010)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-45657-0_10","volume-title":"Computer Aided Verification","author":"P. Chatterjee","year":"2002","unstructured":"Chatterjee, P., Sivaraj, H., Gopalakrishnan, G.: Shared memory consistency protocol verification against weak memory models: Refinement via model-checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 123\u2013136. Springer, Heidelberg (2002)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Y., Lv, Y., Hu, W., Chen, T., Shen, H., Wang, P., Pan, H.: Fast complete memory consistency verification. In: HPCA, pp. 381\u2013392 (2009)","DOI":"10.1109\/HPCA.2009.4798276"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1353522.1353528","volume-title":"MSPC","author":"N. Chong","year":"2008","unstructured":"Chong, N., Ishtiaq, S.: Reasoning about the ARM weakly consistent memory model. In: MSPC, pp. 16\u201319. ACM, New York (2008)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2005","unstructured":"Een, N., Sorensson, N.: Minisat - a SAT solver with conflict-clause minimization. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569. Springer, Heidelberg (2005)"},{"key":"26_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Heidelberg (1996)"},{"issue":"2","key":"26_CR13","first-page":"114","volume":"32","author":"S. Hangal","year":"2004","unstructured":"Hangal, S., Vahia, D., Manovit, C., Lu, J.Y.J.: TSOtool: A program for verifying memory systems using the memory consistency model. ISCA\u00a032(2), 114 (2004)","journal-title":"ISCA"},{"key":"26_CR14","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, 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR15","unstructured":"Intel Corporation: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (March 2010)"},{"issue":"9","key":"26_CR16","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Transactions on Computers\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Transactions on Computers"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Mador-Haim, S., Alur, R., Martin, M.: Generating litmus tests for contrasting memory consistency models - extended version. Technical report, Dept. of Computer Information Science, U. of Pennsylvania (2010)","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: POPL, pp. 378\u2013391 (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BFb0028767","volume-title":"Computer Aided Verification","author":"R. Nalumasu","year":"1998","unstructured":"Nalumasu, R., Ghughal, R., Mokkedem, A., Gopalakrishnan, G.: The \u2019test model-checking\u2019 approach to the verification of formal memory models of multiprocessors. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 464\u2013476. Springer, Heidelberg (1998)"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: TPHOLs, pp. 391\u2013407 (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers\u00a048 (1999)","DOI":"10.1109\/12.752664"},{"key":"26_CR22","volume-title":"The SPARC Architecture Manual Version 9","author":"D.L. Weaver","year":"1994","unstructured":"Weaver, D.L., Germond, T.: The SPARC Architecture Manual Version 9. Prentice Hall PTR, Englewood Cliffs (1994)"},{"issue":"5-6","key":"26_CR23","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1002\/cpe.837","volume":"17","author":"Y. Yang","year":"2005","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: UMM: an operational memory model specification framework with integrated model checking capability. Concurr. Comput.: Pract. Exper.\u00a017(5-6), 465\u2013487 (2005)","journal-title":"Concurr. Comput. : Pract. Exper."},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:50:38Z","timestamp":1606186238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}