{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T22:41:31Z","timestamp":1775256091674,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319980461","type":"print"},{"value":"9783319980478","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","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":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_18","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"283-303","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning About Weak Semantics via Strong Semantics"],"prefix":"10.1007","author":[{"given":"Roland","family":"Meyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"18_CR1","unstructured":"Parosh Aziz Abdulla, Bengt Jonsson, and Cong Quy Trinh. \u201cAutomated Verification of Linearization Policies\u201d. In: SAS Vol. 9837. LNCS. Springer, 2016, pp. 61\u201383."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla et al. \u201cAn Integrated Specification and Verification Technique for Highly Concurrent Data Structures\u201d. In: TACAS Vol. 7795. LNCS. Springer, 2013, pp. 324\u2013338.","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"18_CR3","unstructured":"Sarita V. Adve and Mark D. Hill. \u201cA Unified Formalization of Four Shared-Memory Models\u201d. In: IEEE Trans. Parallel Distrib Syst. 4.6 (1993), pp. 613\u2013624."},{"key":"18_CR4","unstructured":"Jade Alglave. \u201cA shared memory poetics\u201d. PhD thesis. Universit\u00e9 Paris 7, 2010."},{"key":"18_CR5","unstructured":"Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. \u201cChecking and Enforcing Robustness against TSO\u201d. In: ESOP Vol. 7792. LNCS. Springer, 2013, pp. 533\u2013553."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. \u201cChecking Robustness against TSO\u201d. In: CoRR abs\/1208.6152 (2012).","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"18_CR7","unstructured":"Ahmed Bouajjani, Roland Meyer, and Eike M\u00f6hlmann. \u201cDeciding Robustness against Total Store Ordering\u201d. In: ICALP (2). Vol. 6756. LNCS. Springer, 2011, pp. 428\u2013440."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani et al. \u201cLazy TSO Reachability\u201d. In: FASE Vol. 9033. LNCS. Springer, 2015, pp. 267\u2013282.","DOI":"10.1007\/978-3-662-46675-9_18"},{"key":"18_CR9","unstructured":"Sebastian Burckhardt and Madanlal Musuvathi. \u201cEffective Program Verification for Relaxed Memory Models\u201d. In: CAV Vol. 5123. LNCS. Springer, 2008, pp. 107\u2013120."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke. \u201cThe Birth of Model Checking\u201d. In: 25 Years of Model Checking. Vol. 5000. LNCS. Springer, 2008, pp. 1\u201326.","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"18_CR11","unstructured":"Patrick Cousot and Radhia Cousot. \u201cAbstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints\u201d. In: POPL ACM, 1977, pp. 238\u2013252."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. \u201cSystematic Design of Program Analysis Frameworks\u201d. In: POPL ACM Press, 1979, pp. 269\u2013282.","DOI":"10.1145\/567752.567778"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Edsger W. Dijkstra. \u201cCooperating Sequential Processes\u201d. In: The Origin of Concurrent Programming: From Semaphores to Remote Procedure Calls. Ed. by Per Brinch Hansen. Springer New York, 2002, pp. 65\u2013138.","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Simon Doherty et al. \u201cFormal Verification of a Practical Lock-Free Queue Algorithm\u201d. In: FORTE. Vol. 3235. LNCS. Springer, 2004, pp. 97\u2013114.","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. \u201cA calculus of atomic actions\u201d. In: POPL ACM, 2009, pp. 2\u201315.","DOI":"10.1145\/1594834.1480885"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Tayfun Elmas et al. \u201cSimplifying Linearizability Proofs with Reduction and Abstraction\u201d. In: TACAS Vol. 6015. LNCS. Springer, 2010, pp. 296\u2013311.","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Timothy L. Harris. \u201cA Pragmatic Implementation of Non-blocking Linked-Lists\u201d. In: DISC Vol. 2180. LNCS. Springer, 2001, pp. 300\u2013314.","DOI":"10.1007\/3-540-45414-4_21"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Haziza et al. \u201cPointer Race Freedom\u201d. In: CoRR abs\/1511.00184 (2015).","DOI":"10.1007\/978-3-662-49122-5_19"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Haziza et al. \u201cPointer Race Freedom\u201d. In: VMCAI Vol. 9583. LNCS. Springer, 2016, pp. 393\u2013412.","DOI":"10.1007\/978-3-662-49122-5_19"},{"key":"18_CR20","unstructured":"Maurice Herlihy and Nir Shavit. The art of multiprocessor programming. Morgan Kaufmann, 2008."},{"key":"18_CR21","unstructured":"Luk\u00e1s Hol\u0131ik et al. \u201cEffect Summaries for Thread-Modular Analysis\u201d. In: CoRR abs\/1705.03701 (2017)."},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Luk\u00e1s Hol\u0131ik et al. \u201cEffect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic\u201d. In: SAS Vol. 10422. LNCS. Springer, 2017, pp. 169\u2013191.","DOI":"10.1007\/978-3-319-66706-5_9"},{"key":"18_CR23","unstructured":"Thuan Quang Huynh and Abhik Roychoudhury. \u201cA Memory Model Sensitive Checker for C#\u201d. In: FM Vol. 4085. LNCS. Springer, 2006, pp. 476\u2013491."},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Bengt Jonsson. \u201cUsing refinement calculus techniques to prove linearizability\u201d. In: Formal Asp. Comput. 24.4-6 (2012), pp. 537\u2013554.","DOI":"10.1007\/s00165-012-0250-7"},{"issue":"1","key":"18_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"Leslie Lamport","year":"1987","unstructured":"Leslie Lamport. \u201cA Fast Mutual Exclusion Algorithm\u201d. In: ACM Trans. Comput. Syst. 5.1 (1987), pp. 1\u201311.","journal-title":"ACM Transactions on Computer Systems"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Leslie Lamport. \u201cHow to Make a Multiprocessor Computer That Correctly Executes Multi- process Programs\u201d. In: IEEE Trans. Computers 28.9 (1979), pp. 690\u2013691.","DOI":"10.1109\/TC.1979.1675439"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Maged M. Michael. \u201cHigh performance dynamic lock-free hash tables and list-based sets\u201d. In: SPAA 2002, pp. 73\u201382.","DOI":"10.1145\/564879.564881"},{"key":"18_CR28","unstructured":"Maged M. Michael and Michael L. Scott. \u201cNonblocking Algorithms and Preemption-Safe Locking on Multiprogrammed Shared Memory Multiprocessors\u201d. In: J. Parallel Distrib Comput. 51.1 (1998), pp. 1\u201326."},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Maged M. Michael and Michael L. Scott. \u201cSimple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms\u201d. In: PODC ACM, 1996, pp. 267\u2013275.","DOI":"10.21236\/ADA309412"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Seungjoon Park and David L. Dill. \u201cAn Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order)\u201d. In: SPAA. 1995, pp. 34\u201341.","DOI":"10.1145\/215399.215413"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Gary L. Peterson. \u201cMyths About the Mutual Exclusion Problem\u201d. In: Inf Process. Lett. 12.3 (1981), pp. 115\u2013116.","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"18_CR32","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. \u201cTaDA: A Logic for Time and Data Abstraction\u201d. In: ECOOP Vol. 8586. LNCS. Springer, 2014, pp. 207\u2013231."},{"issue":"4","key":"18_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2629496","volume":"15","author":"Gerhard Schellhorn","year":"2014","unstructured":"Gerhard Schellhorn, John Derrick, and Heike Wehrheim. \u201cA Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures\u201d. In: ACM Trans. Comput. Log. 15.4 (2014), 31:1\u201331:37.","journal-title":"ACM Transactions on Computational Logic"},{"key":"18_CR34","unstructured":"Peter Sewell et al. \u201cx86-TSO: a rigorous and usable programmer\u2019s model for x86 multipro- cessors\u201d. In: Commun. ACM 53.7 (2010), pp. 89\u201397."},{"key":"18_CR35","unstructured":"Dennis E. Shasha and Marc Snir. \u201cEfficient and Correct Execution of Parallel Programs that Share Memory\u201d. In: ACM Trans. Program. Lang Syst. 10.2 (1988), pp. 282\u2013312."},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Viktor Vafeiadis. \u201cRGSep Action Inference\u201d. In: VMCAI Vol. 5944. LNCS. Springer, 2010, pp. 345\u2013361.","DOI":"10.1007\/978-3-642-11319-2_25"},{"key":"18_CR37","unstructured":"Viktor Vafeiadis and Matthew J. Parkinson. \u201cA Marriage of Rely\/Guarantee and Separation Logic\u201d. In: CONCUR Vol. 4703. LNCS. Springer, 2007, pp. 256\u2013271."},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"Martin T. Vechev and Eran Yahav. \u201cDeriving linearizable fine-grained concurrent objects\u201d. In: PLDI ACM, 2008, pp. 125\u2013135.","DOI":"10.1145\/1379022.1375598"},{"key":"18_CR39","unstructured":"Eran Yahav and Shmuel Sagiv. \u201cAutomatically Verifying Concurrent Queue Algorithms\u201d. In: Electr Notes Theor Comput. Sci. 89.3 (2003), pp. 450\u2013463."}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T21:20:38Z","timestamp":1775251238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_18","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}