{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T16:54:19Z","timestamp":1793033659486,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287558","type":"print"},{"value":"9783642287565","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_15","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"204-219","source":"Crossref","is-referenced-by-count":39,"title":["Counter-Example Guided Fence Insertion under TSO"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carl","family":"Leonardsson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Adve, S., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer\u00a029(12) (1996)","DOI":"10.1109\/2.546611"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-22110-1_6","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L.: Stability in Weak Memory Models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 50\u201366. Springer, Heidelberg (2011)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL (2010)","DOI":"10.1145\/1706299.1706303"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting Rid of Store-Buffers in TSO Analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.: CheckFence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11817963_45","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2006","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 489\u2013502. Springer, Heidelberg (2006)"},{"key":"15_CR8","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":"15_CR9","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. Technical Report UCB\/EECS-2010-32, UCB (2010)","DOI":"10.1145\/2001420.2001436"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-19835-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 11\u201325. Springer, Heidelberg (2011)"},{"key":"15_CR11","volume-title":"Cooperating sequential processes","author":"E.W. Dijkstra","year":"2002","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. Springer-Verlag New York, Inc., New York (2002)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: ICS. ACM (2003)","DOI":"10.1145\/782814.782854"},{"key":"15_CR13","unstructured":"Fraser, K.: Practical lock-freedom. Technical Report UCAM-CL-TR-579, University of Cambridge, Computer Laboratory (2004)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Hensgen, D., Finkel, R., Manber, U.: Two algorithms for barrier synchronization. IJPP 17 (February 1988)","DOI":"10.1007\/BF01379320"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7) (1952)","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11813040_32","volume-title":"FM 2006: Formal Methods","author":"T.Q. Huynh","year":"2006","unstructured":"Huynh, T.Q., Roychoudhury, A.: A Memory Model Sensitive Checker for C#. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 476\u2013491. Springer, Heidelberg (2006)"},{"key":"15_CR17","unstructured":"I.\u00a0Inc. IntelTM64 and IA-32 Architectures Software Developer\u2019s Manuals"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2011)","DOI":"10.1145\/2261417.2261438"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI (2011)","DOI":"10.1145\/1993498.1993521"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. CACM 17 (August 1974)","DOI":"10.1145\/361082.361093"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A fast mutual exclusion algorithm (1986)","DOI":"10.1145\/5383.5385"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Linden, A., Wolper, P.: An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 212\u2013226. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16164-3_16"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Linden, A., Wolper, P.: A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol.\u00a06823, pp. 144\u2013160. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22306-8_10"},{"key":"15_CR24","unstructured":"Lynch, N., Patt-Shamir, B.: Distributed Algorithms, Lecture Notes for 6.852 FALL 1992. Technical report, MIT, Cambridge, MA, USA (1993)"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Magnusson, P., Landin, A., Hagersten, E.: Queue locks on cache coherent multiprocessors. In: IPPS. IEEE Computer Society (1994)","DOI":"10.1109\/IPPS.1994.288305"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9 (February 1991)","DOI":"10.1145\/103727.103729"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S. Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 478\u2013503. Springer, Heidelberg (2010)"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Owens","year":"2009","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A Better x86 Memory Model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Peterson, G.L.: Myths About the Mutual Exclusion Problem. IPL 12(3) (1981)","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-tso: A rigorous and usable programmer\u2019s model for x86 multiprocessors. CACM 53 (2010)","DOI":"10.1145\/1785414.1785443"},{"key":"15_CR31","unstructured":"Weaver, D., Germond, T. (eds.): The SPARC Architecture Manual Version 9. PTR Prentice Hall (1994)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T02:09:54Z","timestamp":1641434994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}