{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T10:10:16Z","timestamp":1769076616573,"version":"3.49.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319479576","type":"print"},{"value":"9783319479583","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-47958-3_4","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T13:40:52Z","timestamp":1475934052000},"page":"63-84","source":"Crossref","is-referenced-by-count":6,"title":["Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models"],"prefix":"10.1007","author":[{"given":"Tatsuya","family":"Abe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshiyuki","family":"Maeda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. J. Inf. Process. (2016, to appear)","DOI":"10.2197\/ipsjjip.25.244"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. Int. J. Softw. Tools Technol. Transferr (2016, to appear). doi: 10.1007\/s10009-016-0429-y","DOI":"10.1007\/s10009-016-0429-y"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Abe, T., Ugawa, T., Maeda, T., Matsumoto, K.: Reducing state explosion for software model checking with relaxed memory consistencymodels. In: Proceedings of SETTA. LNCS, vol. 9984 (2016, to appear). doi: 10.1007\/978-3-319-47677-3_8","DOI":"10.1007\/978-3-319-47677-3_8"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of PLDI, pp. 68\u201378 (2008)","DOI":"10.1145\/1375581.1375591"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: Proceedings of POPL, pp. 392\u2013403 (2009)","DOI":"10.1145\/1594834.1480930"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Boudol, G., Petri, G., Serpette, B.P.: Relaxed operational semantics of concurrent programming languages. In: Proceedings of EXPRESS\/SOS, pp. 19\u201333 (2012)","DOI":"10.4204\/EPTCS.89.3"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-11957-6_15","volume-title":"Programming Languages and Systems","author":"R Ferreira","year":"2010","unstructured":"Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267\u2013286. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_15"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580, 583 (1969)","DOI":"10.1145\/363235.363259"},{"issue":"6","key":"4_CR9","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1016\/j.jlap.2011.04.005","volume":"80","author":"T Hoare","year":"2011","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebraic Program 80(6), 266\u2013296 (2011)","journal-title":"J. Log. Algebraic Program"},{"key":"4_CR10","volume-title":"The SPIN Model Checker","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)"},{"key":"4_CR11","unstructured":"Intel Corporation: A Formal Specification of Intel Itanium Processor Family Memory Ordering (2002)"},{"key":"4_CR12","unstructured":"ISO, IEC 14882: 2011: Programming Language C++ (2011)"},{"key":"4_CR13","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University (1981)"},{"issue":"5","key":"4_CR14","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1145\/1556444.1556453","volume":"36","author":"B Jonsson","year":"2008","unstructured":"Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings: (preliminary version). SIGARCH Comput. Archit. News 36(5), 65\u201371 (2008)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-662-47666-6_25","volume-title":"Automata, Languages, and Programming","author":"O Lahav","year":"2015","unstructured":"Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311\u2013323. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-47666-6_25"},{"issue":"3","key":"4_CR16","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM TOPLAS 16(3), 872\u2013923 (1994)","journal-title":"ACM TOPLAS"},{"key":"4_CR17","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: Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212\u2013226. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16164-3_16"},{"key":"4_CR18","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"JJC Meyer","year":"2004","unstructured":"Meyer, J.J.C.: Modal epistemic and doxastic logic. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 10, 2nd edn, pp. 1\u201338. Springer, Dordrecht (2004)","edition":"2"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-36575-3_24","volume-title":"Programming Languages and Systems","author":"LP Nieto","year":"2003","unstructured":"Nieto, L.P.: The rely-guarantee method in Isabelle\/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348\u2013362. Springer, Heidelberg (2003). doi: 10.1007\/3-540-36575-3_24"},{"key":"4_CR20","unstructured":"Oracle Corporation: The Java Language Specification. Java SE 8 Edition (2015)"},{"key":"4_CR21","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. 6183, pp. 478\u2013503. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14107-2_23"},{"key":"4_CR22","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. 5674, pp. 391\u2013407. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_27"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15057-9_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T Ridge","year":"2010","unstructured":"Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55\u201370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15057-9_4"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of PLDI, pp. 175\u2013186 (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Proceedings of POPL, pp. 379\u2013391 (2008)","DOI":"10.1145\/1480881.1480929"},{"issue":"7","key":"4_CR26","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","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. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"4_CR27","unstructured":"SPARC International Inc.: The SPARC Architecture Manual, Version 9 (1994)"},{"key":"4_CR28","unstructured":"St\u00f8len, K.: Development of parallel programs on shared data-structures. Technical report UMCS-91-1-1, Department of Computer Science, University of Manchester (1991)"},{"key":"4_CR29","unstructured":"Tofan, B., Schellhorn, G., B\u00e4umler, S., Reif, W.: Embedding rely-guarantee reasoning in temporal logic. Technical report, Institut f\u00fcr Informatik, Universit\u00e4t Augsburg (2010)"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: Proceedings of OOPSLA. 691\u2013707(2014)","DOI":"10.1145\/2714064.2660243"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Formal reasoning about the C11 weak memory model. In: Proceedings of CPP (2015)","DOI":"10.1145\/2676724.2693181"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: Proceedings of OOPSLA, pp. 867\u2013884 (2013)","DOI":"10.1145\/2509136.2509532"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-19797-5_2","volume-title":"Mathematics of Program Construction","author":"S Staden","year":"2015","unstructured":"Staden, S.: On rely-guarantee reasoning. In: Hinze, R., Voigtl\u00e4nder, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 30\u201349. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-19797-5_2"},{"key":"4_CR34","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"},{"key":"4_CR35","unstructured":"Xu, Q.: A theory of state-based parallel programming. Ph.D. thesis, Oxford University Computing Laboratory (1992)"},{"issue":"2","key":"4_CR36","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149\u2013174 (1997)","journal-title":"Formal Aspects Comput."}],"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-319-47958-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T11:30:58Z","timestamp":1568460658000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}