{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:00Z","timestamp":1774025820062,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466681","type":"print"},{"value":"9783662466698","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46669-8_30","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T14:37:37Z","timestamp":1427899057000},"page":"736-761","source":"Crossref","is-referenced-by-count":13,"title":["A Separation Logic for Fictional Sequential Consistency"],"prefix":"10.1007","author":[{"given":"Filip","family":"Sieczkowski","sequence":"first","affiliation":[]},{"given":"Kasper","family":"Svendsen","sequence":"additional","affiliation":[]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"Intel threading building blocks documentation: Fenced data transfer, \n                    \n                      https:\/\/software.intel.com\/en-us\/node\/506122\n                    \n                    \n                   (accessed: June 25, 2014)"},{"key":"30_CR2","unstructured":"java.util.concurrent API, \n                    \n                      http:\/\/docs.oracle.com\/javase\/7\/docs\/api\/java\/util\/concurrent\/package-summary.html\n                    \n                    \n                   (accessed: June 25, 2014)"},{"key":"30_CR3","unstructured":"Linux kernel mailing list, spin_unlock optimization(i386) (November 1999)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 141\u2013157. Springer, Heidelberg (2013)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-Hyperdoctrines, Higher-order Separation Logic, and Abstraction. ACM TOPLAS (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Birkedal, L., et al.: First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. In: Proc. of LICS (2011)","DOI":"10.1109\/LICS.2011.16"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated Verification of Low-level Programs in Computational Separation Logic. In: Proc. of PLDI (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-642-14052-5_28","volume-title":"Interactive Theorem Proving","author":"E. Cohen","year":"2010","unstructured":"Cohen, E., Schirmer, B.: From total store order to sequential consistency: A practical reduction theorem. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 403\u2013418. Springer, Heidelberg (2010)"},{"key":"30_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P. Rocha Pinto da","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: A logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol.\u00a08586, pp. 207\u2013231. Springer, Heidelberg (2014)"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: Compositional Reasoning for Concurrent Programs. In: Proc. of POPL (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular Shape Analysis. In: Proc. of PLDI (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show No Weakness: Sequentially Consistent Specifications of TSO Libraries. In: Proc. of DISC (2012)","DOI":"10.1007\/978-3-642-33651-5_3"},{"key":"30_CR14","unstructured":"Howells, D., McKenney, P.E.: Circular buffers, \n                    \n                      https:\/\/www.kernel.org\/doc\/Documentation\/circular-buffers.txt"},{"key":"30_CR15","unstructured":"Jacobs, B.: Verifying TSO Programs. Technical report, Report CW660 (May 2014)"},{"issue":"1","key":"30_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"J.M. Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM TOCS\u00a09(1), 21\u201365 (1991)","journal-title":"ACM TOCS"},{"key":"30_CR17","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":"30_CR18","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.\u00a06217, pp. 55\u201370. Springer, Heidelberg (2010)"},{"key":"30_CR19","unstructured":"Schmidt, D.C., Harrison, T.: Double-checked locking - an optimization pattern for efficiently initializing and accessing thread-safe objects (1997), \n                    \n                      http:\/\/www.dre.vanderbilt.edu\/~schmidt\/PDF\/DC-Locking.pdf"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Sewell, P., Sarkar, S., Owens, S., Zappa Nardelli, F., Myreen, M.O.: x86-TSO: A Rigorous and Usable Programmers Model for x86 Multiprocessors. In: Comm. ACM (2010)","DOI":"10.1145\/1785414.1785443"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Sieczkowski, F., Svendsen, K., Birkedal, L., Pichon-Pharabod, J.: A Separation Logic for Fictional Sequential Consistency. Technical report, Aarhus University (2014), \n                    \n                      http:\/\/cs.au.dk\/~filips\/icap-tso-tr.pdf","DOI":"10.1007\/978-3-662-46669-8_30"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K. Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol.\u00a08410, pp. 149\u2013168. Springer, Heidelberg (2014)"},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation. In: Proc. of OOPSLA (2014)","DOI":"10.1145\/2660193.2660243"},{"key":"30_CR24","unstructured":"Wehrman, I.: Weak-Memory Local Reasoning. PhD thesis, University of Texas, Dissertation draft (2012)"},{"key":"30_CR25","unstructured":"Wickerson, J.: Concurrent verification for sequential programs. PhD thesis, University of Cambridge (2012)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46669-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:18:29Z","timestamp":1559139509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}