{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T22:13:44Z","timestamp":1790460824404,"version":"4.1.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1422471, CCF-1223850, CNS-1514435"],"award-info":[{"award-number":["CCF-1422471, CCF-1223850, CNS-1514435"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n                    We present\n                    <jats:italic>pretend synchrony<\/jats:italic>\n                    , a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their correctness. To do so, we compute a\n                    <jats:italic>synchronization<\/jats:italic>\n                    , a semantically equivalent program where all sends, receives, and message buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style Verification Conditions and SMT. We implement our approach as a framework for writing verified distributed programs in Go and evaluate it with four challenging case studies\u2014 the classic two-phase commit protocol, the Raft leader election protocol, single-decree Paxos protocol, and a Multi-Paxos based distributed key-value store. We find that pretend synchrony allows us to develop performant systems while making verification of functional correctness\n                    <jats:italic>simpler<\/jats:italic>\n                    by reducing manually specified invariants by a factor of 6, and\n                    <jats:italic>faster<\/jats:italic>\n                    , by reducing checking time by three orders of magnitude.\n                  <\/jats:p>","DOI":"10.1145\/3290372","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T08:33:51Z","timestamp":1546590831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["Pretend synchrony: synchronous verification of asynchronous distributed programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Klaus","family":"v. Gleissenthall","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rami G\u00f6khan","family":"K\u0131c\u0131","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Bakst","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535845"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133934"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/PGEC.1966.264565"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Ken McMillan and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS.  Nikolaj Bj\u00f8rner Ken McMillan and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS.","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"e_1_2_2_5_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II . 372\u2013391","author":"Bouajjani Ahmed","year":"2018","unstructured":"Ahmed Bouajjani , Constantin Enea , Kailiang Ji , and Shaz Qadeer . 2018 . On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In Computer Aided Verification - 30th International Conference , CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II . 372\u2013391 . Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. 2018. On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II . 372\u2013391."},{"key":"e_1_2_2_6_1","volume-title":"Sipma","author":"Bradley Aaron R.","year":"2006","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B . Sipma . 2006 . What\u2019s Decidable About Arrays?. In VMCAI. Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What\u2019s Decidable About Arrays?. In VMCAI."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04420-5_10"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.10.006"},{"key":"e_1_2_2_9_1","volume-title":"9th International Conference","author":"Cohen Ernie","year":"1998","unstructured":"Ernie Cohen and Leslie Lamport . 1998 . Reduction in TLA. In CONCUR \u201998: Concurrency Theory , 9th International Conference , Nice, France , September 8-11, 1998, Proceedings . 317\u2013331. Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In CONCUR \u201998: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings . 317\u2013331."},{"key":"e_1_2_2_10_1","volume-title":"Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4","author":"Deni\u00e9lou Pierre-Malo","year":"2012","unstructured":"Pierre-Malo Deni\u00e9lou , Nobuko Yoshida , Andi Bejleri , and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 ( 2012 ). Pierre-Malo Deni\u00e9lou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. 2012. Parameterised Multiparty Session Types. Logical Methods in Computer Science 8, 4 (2012)."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660211"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786861"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_24"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2414639.2414658"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837650"},{"key":"e_1_2_2_17_1","unstructured":"C. Dragoi and J. Widder. 2018. Reducing asynchrony to synchronized rounds. ArXiv e-prints (April 2018). arXiv: cs.PL\/1804.07078  C. Dragoi and J. Widder. 2018. Reducing asynchrony to synchronized rounds. ArXiv e-prints (April 2018). arXiv: cs.PL\/1804.07078"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480885"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535885"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040315"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/780822.781169"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908129"},{"key":"e_1_2_2_25_1","volume-title":"Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem","author":"Godefroid Patrice","unstructured":"Patrice Godefroid , J van Leeuwen , J Hartmanis , G Goos , and Pierre Wolper . 1996. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem . Vol. 1032 . Springer Heidelberg . Patrice Godefroid, J van Leeuwen, J Hartmanis, G Goos, and Pierre Wolper. 1996. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem . Vol. 1032. Springer Heidelberg."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_28_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II . 449\u2013465","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel , Erez Petrank , Shaz Qadeer , and Serdar Tasiran . 2015 b. Automated and Modular Refinement Reasoning for Concurrent Programs. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II . 449\u2013465 . Chris Hawblitzel, Erez Petrank, Shaz Qadeer, and Serdar Tasiran. 2015b. Automated and Modular Refinement Reasoning for Concurrent Programs. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II . 449\u2013465."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009893"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Kohei Honda. 1993. Types for dyadic interaction. In CONCUR.   Kohei Honda. 1993. Types for dyadic interaction. In CONCUR.","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33518-1_37"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_33_1","volume-title":"4th Symposium on Networked Systems Design and Implementation (NSDI 2007), April 11-13, 2007, Cambridge, Massachusetts, USA, Proceedings.","author":"Killian Charles Edwin","year":"2007","unstructured":"Charles Edwin Killian , James W. Anderson , Ranjit Jhala , and Amin Vahdat . 2007 . Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code . In 4th Symposium on Networked Systems Design and Implementation (NSDI 2007), April 11-13, 2007, Cambridge, Massachusetts, USA, Proceedings. Charles Edwin Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In 4th Symposium on Networked Systems Design and Implementation (NSDI 2007), April 11-13, 2007, Cambridge, Massachusetts, USA, Proceedings."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"e_1_2_2_36_1","volume-title":"Henzinger","author":"Kragl Bernhard","year":"2018","unstructured":"Bernhard Kragl , Shaz Qadeer , and Thomas A . Henzinger . 2018 . Synchronizing the Asynchronous. In CONCUR. Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. 2018. Synchronizing the Asynchronous. In CONCUR."},{"key":"e_1_2_2_37_1","volume-title":"Paxos Made Simple. (December","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport . 2001. Paxos Made Simple. (December 2001 ), 51\u201358. https:\/\/www.microsoft.com\/en-us\/research\/publication\/ paxos-made-simple\/ Leslie Lamport. 2001. Paxos Made Simple. (December 2001), 51\u201358. https:\/\/www.microsoft.com\/en-us\/research\/publication\/ paxos-made-simple\/"},{"key":"e_1_2_2_38_1","unstructured":"Leslie Lamport Dahlia Malkhi and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. Microsoft Research.  Leslie Lamport Dahlia Malkhi and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. Microsoft Research."},{"key":"e_1_2_2_39_1","volume-title":"Sturgis","author":"Lampson Butler","year":"1976","unstructured":"Butler Lampson and Howard E . Sturgis . 1976 . Crash Recovery in a Distributed Data Storage System. In Technical report XEROX Palo Alto Research Center . Butler Lampson and Howard E. Sturgis. 1976. Crash Recovery in a Distributed Data Storage System. In Technical report XEROX Palo Alto Research Center ."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180157"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","unstructured":"K. R. M. Leino and C. Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers. In CAV.  K. R. M. Leino and C. Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers. In CAV.","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_45_1","volume-title":"Bad Herrenalb","author":"McMillan Kenneth L.","year":"1999","unstructured":"Kenneth L. McMillan . 1999 . Verification of Infinite State Systems by Compositional Model Checking. In Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME \u201999 , Bad Herrenalb , Germany, September 27-29, 1999, Proceedings . 219\u2013234. Kenneth L. McMillan. 1999. Verification of Infinite State Systems by Compositional Model Checking. In Correct Hardware Design and Verification Methods, 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME \u201999, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings . 219\u2013234."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_13"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2517350"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625968"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643666"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734286"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_12"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/383059.383071"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_2_2_60_1","unstructured":"Nissim Francez Tzilla Elrad. 1982. Decomposition of distributed programs into communication-closed layers. In Science of Computer Programming .  Nissim Francez Tzilla Elrad. 1982. Decomposition of distributed programs into communication-closed layers. In Science of Computer Programming ."},{"key":"e_1_2_2_61_1","unstructured":"James R. Wilcox Ilya Sergey and Zachary Tatlock. 2017. Programming Language Abstractions for Modularly Verified Distributed Systems. In SNAPL.  James R. Wilcox Ilya Sergey and Zachary Tatlock. 2017. Programming Language Abstractions for Modularly Verified Distributed Systems. In SNAPL."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_2_64_1","volume-title":"Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2009","author":"Yang Junfeng","year":"2009","unstructured":"Junfeng Yang , Tisheng Chen , Ming Wu , Zhilei Xu , Xuezheng Liu , Haoxiang Lin , Mao Yang , Fan Long , Lintao Zhang , and Lidong Zhou . 2009 . MODIST: Transparent Model Checking of Unmodified Distributed Systems . In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2009 , April 22-24, 2009, Boston, MA, USA . 213\u2013228. Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou. 2009. MODIST: Transparent Model Checking of Unmodified Distributed Systems. In Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2009, April 22-24, 2009, Boston, MA, USA . 213\u2013228."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290372","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290372","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290372","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:58:04Z","timestamp":1750193884000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290372"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290372"],"URL":"https:\/\/doi.org\/10.1145\/3290372","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}