{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:15Z","timestamp":1784830875305,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3385980","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"227-242","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Inductive sequentialization of asynchronous programs"],"prefix":"10.1145","author":[{"given":"Bernhard","family":"Kragl","sequence":"first","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[{"name":"IRIF, France \/ University of Paris, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suha Orhun","family":"Mutluergil","sequence":"additional","affiliation":[{"name":"IRIF, France \/ University of Paris, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[{"name":"Calibra, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2020. Boogie. https:\/\/github.com\/boogie-org\/boogie"},{"key":"e_1_3_2_1_2_1","volume-title":"Rami G\u00f6khan Kici, and Ranjit Jhala","author":"Bakst Alexander","year":"2017","unstructured":"Alexander Bakst, Klaus von Gleissenthall, Rami G\u00f6khan Kici, and Ranjit Jhala. 2017. Verifying distributed programs via canonical sequentialization. In OOPSLA. Inductive Sequentialization of Asynchronous Programs PLDI \u201920, June 15\u201320, 2020, London, UK"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani and Michael Emmi. 2012. Bounded Phase Analysis of Message-Passing Programs. In TACAS. 3-642-28756-5_31 10.1007\/978-3-642-28756-5_31","DOI":"10.1007\/978-3-642-28756-5_31"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_7"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Michael Emmi and Gennaro Parlato. 2011. On Sequentializing Concurrent Programs. In SAS. 978-3-642-23702-7_13 10.1007\/978-3-642-23702-7_13","DOI":"10.1007\/978-3-642-23702-7_13"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Constantin Enea Kailiang Ji and Shaz Qadeer. 2018. On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In CAV. 96142-2_23 10.1007\/978-3-319-96142-2_23","DOI":"10.1007\/978-3-319-96142-2_23"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"David Castro Raymond Hu Sung-Shik Jongmans Nicholas Ng and Nobuko Yoshida. 2019. Distributed programming using roleparametric session types in Go: statically-typed endpoint APIs for dynamically-instantiated communication structures. In POPL. 10.1145\/3290342","DOI":"10.1145\/3290342"},{"key":"e_1_3_2_1_9_1","unstructured":"Tej Chajed M. Frans Kaashoek Butler W. Lampson and Nickolai Zeldovich. 2018. Verifying concurrent software using movers in CSPEC. In OSDI. https:\/\/www.usenix.org\/conference\/osdi18\/presentation\/ chajed"},{"key":"e_1_3_2_1_10_1","volume-title":"Chang and Rosemary Roberts","author":"Ernest J.","year":"1979","unstructured":"Ernest J. H. Chang and Rosemary Roberts. 1979. An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes. Commun. ACM 22, 5 (1979)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Ching-Tsun Chou and Eli Gafni. 1988. Understanding and Verifying Distributed Algorithms Using Stratified Decomposition. In PODC. 10.1145\/62546.62556","DOI":"10.1145\/62546.62556"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Andrei Damian Cezara Dragoi Alexandru Militaru and Josef Widder. 2019. Communication-Closed Asynchronous Protocols. In CAV. 10.1007\/978-3-030-25543-5_20","DOI":"10.1007\/978-3-030-25543-5_20"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2009. Generalized efficient array decision procedures. In FMCAD. 1109\/FMCAD.2009.5351142 10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Cezara Dragoi Thomas A. Henzinger and Damien Zufferey. 2016. PSync: a partially synchronous language for fault-tolerant distributed algorithms. In POPL. 10.1145\/2837614.2837650","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Tayfun Elmas Shaz Qadeer and Serdar Tasiran. 2009. A calculus of atomic actions. In POPL. 10.1145\/1480881.1480885","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_3_2_1_16_1","volume-title":"Decomposition of Distributed Programs into Communication-Closed Layers. Sci. Comput. Program. 2, 3","author":"Elrad Tzilla","year":"1982","unstructured":"Tzilla Elrad and Nissim Francez. 1982. Decomposition of Distributed Programs into Communication-Closed Layers. Sci. Comput. Program. 2, 3 (1982)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Michael Emmi Shaz Qadeer and Zvonimir Rakamaric. 2011. Delaybounded scheduling. In POPL. 10.1145\/1926385.1926432","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Cormac Flanagan and Shaz Qadeer. 2003. A type and effect system for atomicity. In PLDI. 10.1145\/781131.781169","DOI":"10.1145\/781131.781169"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Ivan Gavran Filip Niksic Aditya Kanade Rupak Majumdar and Viktor Vafeiadis. 2015. Rely\/Guarantee Reasoning for Asynchronous Programs. In CONCUR. 10.4230\/LIPIcs.CONCUR.2015.483","DOI":"10.4230\/LIPIcs.CONCUR.2015.483"},{"key":"e_1_3_2_1_20_1","unstructured":"Ronghui Gu Zhong Shao Hao Chen Jieung Kim J\u00e9r\u00e9mie Koenig Xiongnan (Newman) Wu Vilhelm Sj\u00f6berg and David Costanzo. 2019."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Building certified concurrent OS kernels. Commun. ACM 62 10 (2019).","DOI":"10.1145\/3356903"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Ronghui Gu Zhong Shao Jieung Kim Xiongnan (Newman) Wu J\u00e9r\u00e9mie Koenig Vilhelm Sj\u00f6berg Hao Chen David Costanzo and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In PLDI. 10.1145\/3192366.3192381","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_1_23_1","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R. Lorch Bryan Parno Michael L. Roberts Srinath T. V. Setty and Brian Zill. 2015."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"IronFleet: proving practical distributed systems correct. In SOSP. 10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Chris Hawblitzel Erez Petrank Shaz Qadeer and Serdar Tasiran. 2015. Automated and Modular Refinement Reasoning for Concurrent Programs. In CAV. 10.1007\/978-3-319-21668-3_26","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_3_2_1_26_1","volume-title":"Specification and Design of (Parallel) Programs. In IFIP Congress.","author":"Jones Cliff B.","year":"1983","unstructured":"Cliff B. Jones. 1983. Specification and Design of (Parallel) Programs. In IFIP Congress."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Johannes Kloos Rupak Majumdar and Viktor Vafeiadis. 2015. Asynchronous Liquid Separation Types. In ECOOP. LIPIcs.ECOOP.2015.396 10.4230\/LIPIcs.ECOOP.2015.396","DOI":"10.4230\/LIPIcs.ECOOP.2015.396"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3754772"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Bernhard Kragl and Shaz Qadeer. 2018. Layered Concurrent Programs. In CAV. 10.1007\/978-3-319-96145-3_5","DOI":"10.1007\/978-3-319-96145-3_5"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.21"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Salvatore La Torre P. Madhusudan and Gennaro Parlato. 2009. Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. In CAV. 10.1007\/978-3-642-02658-4_36","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_7"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_34_1","unstructured":"Leslie Lamport. 2002. Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_36_1","volume-title":"Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12","author":"Lipton Richard J.","year":"1975","unstructured":"Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12 (1975)."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","unstructured":"1145\/361227.361234 10.1145\/361227.361234","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_1_38_1","unstructured":"Jacob R. Lorch Yixuan Chen Manos Kapritsos Bryan Parno Shaz Qadeer Upamanyu Sharma James R. Wilcox and Xueyuan Zhao. 2020."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Armada: Low-Effort Verification of High-Performance Concurrent Programs. In PLDI. 10.1145\/3385412.3385971","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.024"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Wytse Oortwijn Stefan Blom and Marieke Huisman. 2016. Futurebased Static Analysis of Message Passing Programs. In PLACES. 10.4204\/EPTCS.211.7","DOI":"10.4204\/EPTCS.211.7"},{"key":"e_1_3_2_1_42_1","volume-title":"Owicki and David Gries","author":"Susan","year":"1976","unstructured":"Susan S. Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19, 5 (1976)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Oded Padon Giuliano Losa Mooly Sagiv and Sharon Shoham. 2017. Paxos made EPR: decidable reasoning about distributed protocols. In OOPSLA. 10.1145\/3140568","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Oded Padon Kenneth L. McMillan Aurojit Panda Mooly Sagiv and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. In PLDI. 10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. In TACAS. 31980-1_7 10.1007\/978-3-540-31980-1_7","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Shaz Qadeer and Dinghao Wu. 2004. KISS: keep it simple and sequential. In PLDI. 10.1145\/996841.996845","DOI":"10.1145\/996841.996845"},{"key":"e_1_3_2_1_47_1","volume-title":"POPL. 1145\/3158116 PLDI \u201920, June 15\u201320","author":"Sergey Ilya","year":"2020","unstructured":"Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and proving with distributed protocols. In POPL. 1145\/3158116 PLDI \u201920, June 15\u201320, 2020, London, UK Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_27"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2020. The Coq Proof Assistant version 8.11.0. 10.5281\/zenodo.3744225","DOI":"10.5281\/zenodo.3744225"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385980","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3385980","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:14Z","timestamp":1750200074000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385980"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":50,"alternative-id":["10.1145\/3385412.3385980","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3385980","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}