{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:10Z","timestamp":1775873410246,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["1837132"],"award-info":[{"award-number":["1837132"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Verification of asynchronous distributed programs is challenging due to the need to reason about numerous control paths resulting from the myriad interleaving of messages and failures. In this paper, we propose an automated bookkeeping method based on message chains. Message chains reveal structure in asynchronous distributed system executions and can help programmers verify their systems at the message passing level of abstraction. To evaluate our contributions empirically we build a verification prototype for the P programming language that integrates message chains. We use it to verify 16 benchmarks from related work, one new benchmark that exemplifies the kinds of systems our method focuses on, and two industrial benchmarks. We find that message chains are able to simplify existing proofs and our prototype performs comparably to existing work in terms of runtime. We extend our work with support for specification mining and find that message chains provide enough structure to allow existing learning and program synthesis tools to automatically infer meaningful specifications using only execution examples.<\/jats:p>","DOI":"10.1145\/3622876","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"2224-2250","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Message Chains for Distributed System Verification"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0725-9213","authenticated-orcid":false,"given":"Federico","family":"Mora","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9006-0100","authenticated-orcid":false,"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[{"name":"Amazon Web Services, Cupertino, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9032-7661","authenticated-orcid":false,"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Amazon.com Inc.. 2023. Clock-Bound. https:\/\/github.com\/aws\/clock-bound \t\t\t\t  Amazon.com Inc.. 2023. Clock-Bound. https:\/\/github.com\/aws\/clock-bound"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503275"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90041-0"},{"key":"e_1_2_1_4_1","unstructured":"James Aspnes. 2020. Notes on theory of distributed systems. arXiv preprint arXiv:2001.04235. \t\t\t\t  James Aspnes. 2020. Notes on theory of distributed systems. arXiv preprint arXiv:2001.04235."},{"key":"e_1_2_1_5_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org. \t\t\t\t  Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201017"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/319996.319998"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2369047"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1972.5009015"},{"key":"e_1_2_1_11_1","first-page":"76","article-title":"An SMT-LIB format for sequences and regular expressions","volume":"12","author":"Bj\u00f8rner Nikolaj","year":"2012","unstructured":"Nikolaj Bj\u00f8rner , Vijay Ganesh , Rapha\u00ebl Michel , and Margus Veanes . 2012 . An SMT-LIB format for sequences and regular expressions . SMT , 12 (2012), 76 \u2013 86 . Nikolaj Bj\u00f8rner, Vijay Ganesh, Rapha\u00ebl Michel, and Margus Veanes. 2012. An SMT-LIB format for sequences and regular expressions. SMT, 12 (2012), 76\u201386.","journal-title":"SMT"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22102-7_3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_2_1_14_1","article-title":"Hyperproperties","volume":"18","author":"Clarkson Michael R.","year":"2010","unstructured":"Michael R. Clarkson and Fred B. Schneider . 2010 . Hyperproperties . J. Comput. Secur. , 18 , 6 (2010), sep, 1157\u20131210. issn:0926-227X Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur., 18, 6 (2010), sep, 1157\u20131210. issn:0926-227X","journal-title":"J. Comput. Secur."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571203"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146266"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276529"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_23"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132863.1132867"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409005"},{"key":"e_1_2_1_25_1","volume-title":"Programming by example","author":"Halbert Daniel Conrad","unstructured":"Daniel Conrad Halbert . 1984. Programming by example . University of California , Berkeley. Daniel Conrad Halbert. 1984. Programming by example. University of California, Berkeley."},{"key":"e_1_2_1_26_1","volume-title":"Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Hance Travis","year":"2021","unstructured":"Travis Hance , Marijn Heule , Ruben Martins , and Bryan Parno . 2021 . Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21) . USENIX Association, 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019 s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). USENIX Association, 115\u2013131. isbn:978-1-939133-21-2 https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_28_1","volume-title":"Message Sequence Chart (MSC)","author":"ITU-T.","unstructured":"ITU-T. 2011. Message Sequence Chart (MSC) . International Telecommunication Union . ITU-T. 2011. Message Sequence Chart (MSC). International Telecommunication Union."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_15"},{"key":"e_1_2_1_30_1","volume-title":"Parameterized Reasoning for Distributed Systems with Consensus. CoRR, abs\/2004.04613","author":"Jaber Nouraldin","year":"2020","unstructured":"Nouraldin Jaber , Christopher Wagner , Swen Jacobs , Milind Kulkarni , and Roopsha Samanta . 2020. Parameterized Reasoning for Distributed Systems with Consensus. CoRR, abs\/2004.04613 ( 2020 ), arXiv:2004.04613. arxiv:2004.04613 Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, and Roopsha Samanta. 2020. Parameterized Reasoning for Distributed Systems with Consensus. CoRR, abs\/2004.04613 (2020), arXiv:2004.04613. arxiv:2004.04613"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/3437539.3437631"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207169408804252"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_35_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley Longman Publishing Co., Inc. , USA. isbn:032114306X Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA. isbn:032114306X"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054059"},{"key":"e_1_2_1_37_1","unstructured":"G\u00e9rard Le Lann. 1977. Distributed Systems-Towards a Formal Approach.. In IFIP congress. 7 155\u2013160. \t\t\t\t  G\u00e9rard Le Lann. 1977. Distributed Systems-Towards a Formal Approach.. In IFIP congress. 7 155\u2013160."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_2_1_39_1","unstructured":"Lightbend Inc. 2022. Akka. https:\/\/akka.io\/ \t\t\t\t  Lightbend Inc. 2022. Akka. https:\/\/akka.io\/"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_41_1","volume-title":"Distributed Algorithms","author":"Lynch Nancy A.","unstructured":"Nancy A. Lynch . 1996. Distributed Algorithms . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. isbn:9780080504704 Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. isbn:9780080504704"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44798-9_17"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498682"},{"key":"e_1_2_1_46_1","unstructured":"Fabrizio Montesi. 2014. Choreographic programming. IT-Universitetet i K\u00f8benhavn. \t\t\t\t  Fabrizio Montesi. 2014. Choreographic programming. IT-Universitetet i K\u00f8benhavn."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908118"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572282"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02277859"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_24"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_14"},{"key":"e_1_2_1_53_1","volume-title":"Proc. the 7th IBM Symposium on Mathematical Foundations of Computer Science. 191\u2013209","author":"Shinohara Takeshi","year":"1982","unstructured":"Takeshi Shinohara . 1982 . Polynomial time inference of pattern languages and its applications . In Proc. the 7th IBM Symposium on Mathematical Foundations of Computer Science. 191\u2013209 . Takeshi Shinohara. 1982. Polynomial time inference of pattern languages and its applications. In Proc. the 7th IBM Symposium on Mathematical Foundations of Computer Science. 191\u2013209."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"e_1_2_1_56_1","unstructured":"Telefonaktiebolaget LM Ericsson. 2022. Erlang. https:\/\/www.erlang.org\/doc\/index.html \t\t\t\t  Telefonaktiebolaget LM Ericsson. 2022. Erlang. https:\/\/www.erlang.org\/doc\/index.html"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-007-0026-0"},{"key":"e_1_2_1_58_1","volume-title":"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao , Runzhou Tao , Ronghui Gu , Jason Nieh , Suman Jana , and Gabriel Ryan . 2021 . DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21) . USENIX Association, 405\u2013421. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 405\u2013421. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/yao"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622876","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622876","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":57,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622876"],"URL":"https:\/\/doi.org\/10.1145\/3622876","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}