{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:20Z","timestamp":1767928640429,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":66,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,12,2]],"date-time":"2024-12-02T00:00:00Z","timestamp":1733097600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Ministry of Education - Singapore","doi-asserted-by":"publisher","award":["MOE-MOET32021-0001,T1 251RES2108"],"award-info":[{"award-number":["MOE-MOET32021-0001,T1 251RES2108"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Sui Foundation","award":["Sui Academic Research Award 2024"],"award-info":[{"award-number":["Sui Academic Research Award 2024"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3690355","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"34-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Compositional Verification of Composite Byzantine Protocols"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1017-1562","authenticated-orcid":false,"given":"Qiyuan","family":"Zhao","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5378-2815","authenticated-orcid":false,"given":"George","family":"P\u00eerlea","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6953-447X","authenticated-orcid":false,"given":"Karolina","family":"Grzeszkiewicz","sequence":"additional","affiliation":[{"name":"Yale-NUS College, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-7412","authenticated-orcid":false,"given":"Seth","family":"Gilbert","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Ittai Abraham. 2022. Linear PBFT: a gentle introduction to Practical Byzantine Fault Tolerance. https:\/\/decentralizedthoughts.github.io\/2022--11--20-pbft-via-locked-braodcast\/"},{"key":"e_1_3_2_1_2_1","unstructured":"Ittai Abraham. 2022. Provable Broadcast. https:\/\/decentralizedthoughts.github.io\/2022-09--10-provable-broadcast\/"},{"key":"e_1_3_2_1_3_1","unstructured":"Ittai Abraham. 2022. Two Round HotStuff. https:\/\/decentralizedthoughts.github.io\/2022--11--24-two-round-HS\/"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Ittai Abraham Dahlia Malkhi and Alexander Spiegelman. 2019. Asymptotically Optimal Validated Asynchronous Byzantine Agreement. In PODC. ACM. https:\/\/doi.org\/10.1145\/3293611.3331612","DOI":"10.1145\/3293611.3331612"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_3_2_1_6_1","volume-title":"Chainspace: A Sharded Smart Contracts Platform","author":"Al-Bassam Mustafa","year":"2018","unstructured":"Mustafa Al-Bassam, Alberto Sonnino, Shehar Bano, Dave Hrycyszyn, and George Danezis. 2018. Chainspace: A Sharded Smart Contracts Platform. In NDSS. The Internet Society. https:\/\/www.ndss-symposium.org\/wp-content\/uploads\/2018\/02\/ndss2018_09--2_Al-Bassam_paper.pdf"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--54994--7_27"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_3_2_1_9_1","volume-title":"Welch","author":"Attiya Hagit","year":"2004","unstructured":"Hagit Attiya and Jennifer L. Welch. 2004. Distributed computing - fundamentals, simulations, and advanced topics (2. ed.). Wiley."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.DISC.2022.10"},{"key":"e_1_3_2_1_12_1","volume-title":"Languages for Distributed Algorithms (LADA) workshop.","author":"Bickford Mark","year":"2012","unstructured":"Mark Bickford, Robert Constable, and Vincent Rahli. 2012. The Logic of Events, a framework to reason about distributed systems. In Languages for Distributed Algorithms (LADA) workshop."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Gabriel Bracha. 1984. An Asynchronou [(n-1)\/3]-Resilient Consensus Protocol. In PODC. ACM. https:\/\/doi.org\/10.1145\/800222.806743","DOI":"10.1145\/800222.806743"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90054-X"},{"key":"e_1_3_2_1_15_1","volume-title":"Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Master's thesis","author":"Buchman Ethan","year":"2016","unstructured":"Ethan Buchman. 2016. Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Master's thesis. University of Guelph."},{"key":"e_1_3_2_1_16_1","volume-title":"The latest gossip on BFT consensus. CoRR","author":"Buchman Ethan","year":"2018","unstructured":"Ethan Buchman, Jae Kwon, and Zarko Milosevic. 2018. The latest gossip on BFT consensus. CoRR, Vol. abs\/1807.04938 (2018). showeprint[arXiv]1807.04938 http:\/\/arxiv.org\/abs\/1807.04938"},{"key":"e_1_3_2_1_17_1","volume-title":"Casper the Friendly Finality Gadget. CoRR","author":"Buterin Vitalik","year":"2017","unstructured":"Vitalik Buterin and Virgil Griffith. 2017. Casper the Friendly Finality Gadget. CoRR, Vol. abs\/1710.09437 (2017). http:\/\/arxiv.org\/abs\/1710.09437"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-031-06773-0_33"},{"key":"e_1_3_2_1_19_1","volume-title":"Practical Byzantine Fault Tolerance","author":"Castro Miguel","unstructured":"Miguel Castro and Barbara Liskov. 1999. Practical Byzantine Fault Tolerance. In OSDI. USENIX Association. https:\/\/dl.acm.org\/citation.cfm?id=296824"},{"key":"e_1_3_2_1_20_1","unstructured":"Tej Chajed. 2024. TLA in Coq. https:\/\/github.com\/tchajed\/coq-tla."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-009-0084-6"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS53621.2022.00061"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--540--78800--3_24"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_3_2_1_26_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. ACM. https:\/\/doi.org\/10.1145\/2837614.2837650","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/42282.42283"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409005"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R. Lorch Bryan Parno Michael L. Roberts Srinath T. V. Setty and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In SOSP. ACM. https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_31_1","volume-title":"Iris: a Higher-Order Concurrent Separation Logic Framework, implemented and verified in the Coq proof assistant. https:\/\/iris-project.org\/ Online","author":"Project The Iris","year":"2024","unstructured":"The Iris Project. 2022. Iris: a Higher-Order Concurrent Separation Logic Framework, implemented and verified in the Coq proof assistant. https:\/\/iris-project.org\/ Online; last accessed 29 April 2024."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-19(1:5)2023"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Igor V. Konnov Marijana Lazic Helmut Veith and Josef Widder. 2017. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In POPL. ACM. https:\/\/doi.org\/10.1145\/3009837.3009860","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--44914--8_13"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_1_36_1","volume-title":"The TLA Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","unstructured":"Leslie Lamport. 2002. Specifying Systems, The TLA Language and Tools for Hardware and Software Engineers. Addison-Wesley. http:\/\/research.microsoft.com\/users\/lamport\/tla\/book.html"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Mohsen Lesani Christian J. Bell and Adam Chlipala. 2016. Chapar: certified causally consistent distributed key-value stores. In POPL. ACM. https:\/\/doi.org\/10.1145\/2837614.2837622","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Beno^it Libert Marc Joye and Moti Yung. 2014. Born and raised distributively: fully distributed non-interactive adaptively-secure threshold signatures with short shares. In PODC. ACM. https:\/\/doi.org\/10.1145\/2611462.2611498","DOI":"10.1145\/2611462.2611498"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASICS.FMBC.2020.9"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Loi Luu Viswesh Narayanan Chaodong Zheng Kunal Baweja Seth Gilbert and Prateek Saxena. 2016. A Secure Sharding Protocol For Open Blockchains. In CCS. ACM. https:\/\/doi.org\/10.1145\/2976749.2978389","DOI":"10.1145\/2976749.2978389"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00446-014-0240--5"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_3_2_1_46_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. ACM. https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_47_1","unstructured":"Karl Palmskog Milos Gligoric Lucas Pena Brandon Moore and Grigore Rocsu. 2018. Verification of Casper in the Coq proof assistant. (2018). https:\/\/core.ac.uk\/download\/pdf\/161954227.pdf."},{"key":"e_1_3_2_1_48_1","volume-title":"Toychain: Formally Verified Blockchain Consensus. Master's thesis","author":"George","year":"2019","unstructured":"George P^irlea. 2019. Toychain: Formally Verified Blockchain Consensus. Master's thesis. University College London."},{"key":"e_1_3_2_1_49_1","volume-title":"Errors Found in Distributed Protocols. https:\/\/github.com\/dranov\/protocol-bugs-list Online","author":"George","year":"2024","unstructured":"George P^irlea. 2021. Errors Found in Distributed Protocols. https:\/\/github.com\/dranov\/protocol-bugs-list Online; last accessed 29 April 2024."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","unstructured":"George P^irlea and Ilya Sergey. 2018. Mechanising Blockchain Consensus. In CPP. ACM. https:\/\/doi.org\/10.1145\/3167086","DOI":"10.1145\/3167086"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-009--9161--6"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656423"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","unstructured":"Michael K. Reiter. 1994. Secure Agreement Protocols: Reliable and Atomic Group Multicast in Rampart. In CCS. ACM. https:\/\/doi.org\/10.1145\/191177.191194","DOI":"10.1145\/191177.191194"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Upamanyu Sharma Ralf Jung Joseph Tassarotti M. Frans Kaashoek and Nickolai Zeldovich. 2023. Grove: a Separation-Logic Library for Verifying Distributed Systems. In SOSP. ACM. https:\/\/doi.org\/10.1145\/3600006.3613172","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Marcelo Taube Giuliano Losa Kenneth L. McMillan Oded Padon Mooly Sagiv Sharon Shoham James R. Wilcox and Doug Woos. 2018. Modularity for decidability of deductive verification with applications to distributed systems. In PLDI. ACM. https:\/\/doi.org\/10.1145\/3192366.3192414","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_1_60_1","unstructured":"The Coq Development Team. 2024. The Coq Reference Manual -- Release 8.19.0. https:\/\/coq.inria.fr\/doc\/V8.19.0\/refman."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00042"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360564"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293611.3331591"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.12787570"}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","location":"Salt Lake City UT USA","acronym":"CCS '24","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690355","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690355","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:07:27Z","timestamp":1755842847000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":66,"alternative-id":["10.1145\/3658644.3690355","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3690355","relation":{},"subject":[],"published":{"date-parts":[[2024,12,2]]},"assertion":[{"value":"2024-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}