{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T01:01:19Z","timestamp":1769043679757,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319298160","type":"print"},{"value":"9783319298177","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29817-7_13","type":"book-chapter","created":{"date-parts":[[2016,2,3]],"date-time":"2016-02-03T00:46:18Z","timestamp":1454460378000},"page":"144-155","source":"Crossref","is-referenced-by-count":4,"title":["Weak Memory Models as LLVM-to-LLVM Transformations"],"prefix":"10.1007","author":[{"given":"Vladim\u00edr","family":"\u0160till","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","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. 6806, pp. 50\u201366. Springer, Heidelberg (2011)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 7\u201318. ACM, New York, NY, USA (2010)","DOI":"10.1145\/1706299.1706303"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Havel, V.: LTL Model checking of parallel programs with under-approximated TSO memory model. In: Application of Concurrency to System Design (ACSD), pp. 51\u201359. IEEE (2013)","DOI":"10.1109\/ACSD.2013.8"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J Barnat","year":"2013","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Len\u010do, M., Ro\u010dkai, P., \u0160till, V., et al.: DiVinE 3.0 - an explicit-state model checker for multithreaded C & C++ programs. CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"13_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. 5123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"key":"13_CR6","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency in relaxed memory models. In: Technical report UCB\/EECS-2010-31, EECS Department, University of California, Berkeley, March 2010"},{"key":"13_CR7","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR8","series-title":"LLNC","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"D Dill","year":"1996","unstructured":"Dill, D.: The murphi verification system. Computer Aided Verification. LLNC, vol. 1102, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"key":"13_CR9","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 2003), pp. 285\u2013294. ACM (2003)","DOI":"10.1145\/782852.782854"},{"key":"13_CR10","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1145\/1556444.1556453","volume":"36","author":"B Jonsson","year":"2009","unstructured":"Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36, 65\u201371 (2009)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: Programming Language Design and Implementation (PLDI 2011), pp. 187\u2013198. ACM (2011)","DOI":"10.1145\/1993316.1993521"},{"issue":"9","key":"13_CR14","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 programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume-title":"Automata, Languages and Programming","author":"DJ Lehmann","year":"1981","unstructured":"Lehmann, D.J., Pnueli, A., Stavi, J.: Impartiality, justice, fairness: the ethics of concurrent termination. ICALP. LNCS, vol. 115, pp. 264\u2013277. Springer, Heidelberg (1981)"},{"key":"13_CR16","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.) Model Checking Software. LNCS, vol. 6349, pp. 212\u2013226. Springer, Heidelberg (2010)"},{"key":"13_CR17","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 Workshops 2011. LNCS, vol. 6823, pp. 144\u2013160. Springer, Heidelberg (2011)"},{"key":"13_CR18","unstructured":"Mador-Haim, S., Alur, R., Martin, M.M.K.: Specifying relaxed memory models for state exploration tools. In: \n                    \n                      \n                    \n                    $$(EC)^2$$\n                  : Workshop on Exploting Concurrency Eficiently and Correctly (2009)"},{"key":"13_CR19","volume-title":"Memory Barriers: a Hardware View for Software Hackers","author":"PE Mckenney","year":"2009","unstructured":"Mckenney, P.E.: Memory Barriers: a Hardware View for Software Hackers. Linux Technology Center, Beaverton (2009)"},{"key":"13_CR20","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: Formal Methods in Computer-Aided Design, pp. 111\u2013119. IEEE (2010)"},{"issue":"2","key":"13_CR21","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1109\/12.752664","volume":"48","author":"S Park","year":"1999","unstructured":"Park, S., Dill, D.: An executable specification and verifier for relaxed memory order. IEEE Trans. Comput. 48(2), 227\u2013235 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR22","unstructured":"Ro\u010dkai, P.: Model checking software. Disertation thesis, Faculty of Informatics, Masaryk University (2015)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38088-4_1","volume-title":"NASA Formal Methods","author":"P Ro\u010dkai","year":"2013","unstructured":"Ro\u010dkai, P., Barnat, J., Brim, L.: Improved state space reductions for LTL model checking of C and C++ programs. NFM 2013. LNCS, vol. 7871, pp. 1\u201315. Springer, Heidelberg (2013)"},{"key":"13_CR24","unstructured":"Ro\u010dkai, P., Barnat, J., Brim, L.: Model checking C++ with exceptions. In: Automated Verification of Critical Systems, vol. 70 (2014)"},{"key":"13_CR25","unstructured":"CORPORATE SPARC International, Inc.: The SPARC architecture manual (version 9). Prentice-Hall Inc., Upper Saddle River (1994)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-319-14896-0_12","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"V \u0160till","year":"2014","unstructured":"\u0160till, V., Ro\u010dkai, P., Barnat, J.: Context-switch-directed verification in DIVINE. In: Hlin\u011bn\u00fd, P., Dvo\u0159\u00e1k, Z., Jaro\u0161, J., Kofro\u0148, J., Ko\u0159enek, J., Matula, P., Pala, K. (eds.) MEMICS 2014. LNCS, vol. 8934, pp. 135\u2013146. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Mathematical and Engineering Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29817-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T08:39:35Z","timestamp":1559378375000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29817-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319298160","9783319298177"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29817-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}