{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T05:16:25Z","timestamp":1769058985360,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_28","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T14:35:55Z","timestamp":1361198155000},"page":"512-532","source":"Crossref","is-referenced-by-count":89,"title":["Software Verification for Weak Memory via Program Transformation"],"prefix":"10.1007","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Nimal","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"http:\/\/research.microsoft.com\/en-us\/projects\/poirot\/"},{"key":"28_CR2","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":"28_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1995","unstructured":"Adve, S.V., Gharachorloo, K.: Shared Memory Consistency Models: A Tutorial. IEEE Computer\u00a029, 66\u201376 (1995)","journal-title":"IEEE Computer"},{"key":"28_CR4","unstructured":"Alglave, J.: A Shared Memory Poetics. Ph.D. thesis, Universit\u00e9 Paris 7 and INRIA (2010)"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Alglave, J.: A Formal Hierarchy of Weak Memory Models. In: FMSD (2012)","DOI":"10.1007\/s10703-012-0161-5"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-25318-8_21","volume-title":"Programming Languages and Systems","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Kroening, D., Lugton, J., Nimal, V., Tautschnig, M.: Soundness of Data Flow Analyses for Weak Memory Models. In: Yang, H. (ed.) APLAS 2011. LNCS, vol.\u00a07078, pp. 272\u2013288. Springer, Heidelberg (2011)"},{"key":"28_CR7","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":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-14295-6_25","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2010","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 258\u2013272. Springer, Heidelberg (2010)"},{"key":"28_CR9","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":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-28869-2_2","volume-title":"Programming Languages and Systems","author":"M.F. Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What\u2019s Decidable about Weak Memory Models? In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 26\u201346. Springer, Heidelberg (2012)"},{"key":"28_CR11","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":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-642-22012-8_34","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"2011","unstructured":"Bouajjani, A., Meyer, R., M\u00f6hlmann, E.: Deciding Robustness against Total Store Ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 428\u2013440. Springer, Heidelberg (2011)"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.K.: Checkfence: Checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: ICSE. pp. 331\u2013340. ACM (2011)","DOI":"10.1145\/1985793.1985839"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-22110-1_28","volume-title":"Computer Aided Verification","author":"A. Donaldson","year":"2011","unstructured":"Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 356\u2013371. Springer, Heidelberg (2011)"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-22110-1_32","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2011","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A Constraint-Based Verifier for Multi-threaded Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 412\u2013417. Springer, Heidelberg (2011)"},{"key":"28_CR17","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":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-642-28756-5_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2012","unstructured":"Jin, H., Yavuz-Kahveci, T., Sanders, B.A.: Java Memory Model-Aware Model Checking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 220\u2013236. Springer, Heidelberg (2012)"},{"key":"28_CR19","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2010)"},{"key":"28_CR20","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"},{"issue":"7","key":"28_CR21","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1109\/12.599898","volume":"46","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput.\u00a046(7), 779\u2013782 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"28_CR22","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":"28_CR23","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":"28_CR24","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":"28_CR25","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.: An executable specification, analyzer and verifier for RMO. In: SPAA (1995)","DOI":"10.1145\/215399.215413"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding Power multiprocessors. In: PLDI (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. (1972)","DOI":"10.1109\/SWAT.1971.10"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Enumeration of the elementary circuits of a directed graph. SIAM J. Comput. (1973)","DOI":"10.1137\/0202017"},{"key":"28_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-30482-1_11","volume-title":"Formal Methods and Software Engineering","author":"Y. Yang","year":"2004","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G.: Memory-Model-Sensitive Data Race Analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 30\u201345. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T04:21:05Z","timestamp":1557548465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}