{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,17]],"date-time":"2026-09-17T04:07:12Z","timestamp":1789618032948,"version":"build-2803163510"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642367410","type":"print"},{"value":"9783642367427","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36742-7_37","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:41:56Z","timestamp":1361216516000},"page":"530-536","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Memorax, a Precise and Sound Tool for Automatic 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":"37_CR1","unstructured":"MathSAT4, \n                    \n                      http:\/\/mathsat4.disi.unitn.it\/"},{"key":"37_CR2","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: \n                    \n                      https:\/\/github.com\/memorax\/memorax"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-33125-1_13","volume-title":"Static Analysis","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Automatic Fence Insertion in Integer Programs via Predicate Abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 164\u2013180. Springer, Heidelberg (2012)"},{"key":"37_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-28756-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-Example Guided Fence Insertion under TSO. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 204\u2013219. Springer, Heidelberg (2012)"},{"key":"37_CR5","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":"37_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":"37_CR7","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., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 476\u2013491. Springer, Heidelberg (2006)"},{"key":"37_CR8","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":"37_CR9","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":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-16164-3_16","volume-title":"Model Checking Software","author":"A. Linden","year":"2010","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)"},{"key":"37_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-22306-8_10","volume-title":"Model Checking Software","author":"A. Linden","year":"2011","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)"},{"key":"37_CR12","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":"37_CR13","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. Transactions on Programming Languages and Systems\u00a010, 282\u2013312 (1988)","journal-title":"Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36742-7_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T00:05:56Z","timestamp":1590969956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36742-7_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642367410","9783642367427"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36742-7_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}