{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T02:47:14Z","timestamp":1777949234820,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":25,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819578252","type":"print"},{"value":"9789819578269","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-7826-9_19","type":"book-chapter","created":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T22:28:21Z","timestamp":1777847301000},"page":"363-382","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Program Logic for\u00a0Byzantine-Fault-Tolerant Protocols"],"prefix":"10.1007","author":[{"given":"Yuwen","family":"Kuang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongjin","family":"Liang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,1]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Gramoli, V., Konnov, I., Lazi\u0107, M., Tholoniat, P., Widder, J.: Holistic verification of blockchain consensus. In: Scheideler, C. (ed.) 36th International Symposium on Distributed Computing (DISC 2022), vol. 246, pp. 10:1\u201310:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.DISC.2022.10","DOI":"10.1145\/3519270.3538468"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Carr, H., Jenkins, C., Moir, M., Miraldo, V.C., Silva, L.: Towards formal verification of hotstuff-based byzantine fault tolerant consensus in agda. In: NASA Formal Methods: 14th International Symposium. NFM 2022, Pasadena, CA, USA, May 24\u201327, 2022, Proceedings, pp. 616\u2013635. Springer, Heidelberg (2022)","DOI":"10.1007\/978-3-031-06773-0_33"},{"key":"19_CR3","unstructured":"Castro, M., Liskov, B.H.: A correctness proof for a practical byzantine-fault-tolerant replication algorithm. Tech. rep., USA (1999). https:\/\/publications.csail.mit.edu\/lcs\/pubs\/pdf\/MIT-LCS-TM-597.pdf"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Cirisci, B., Enea, C., Mutluergil, S.O.: Quorum tree abstractions of consensus protocols. In: Proceedings of 32nd European Symposium on Programming (ESOP 2023), pp. 337\u2013362. Springer, Heidelberg (2023)","DOI":"10.1007\/978-3-031-30044-8_13"},{"key":"19_CR5","unstructured":"Cohen, S., Keidar, I.: Tame the wild with byzantine linearizability: reliable broadcast, snapshots, and asset transfer. In: Gilbert, S. (ed.) 35th International Symposium on Distributed Computing (DISC 2021), vol. 209, pp. 18:1\u201318:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021)"},{"issue":"51\u201352","key":"19_CR6","doi-asserted-by":"publisher","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","volume":"411","author":"I Filipovi\u0107","year":"2010","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theoret. Comput. Sci. 411(51\u201352), 4379\u20134398 (2010)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: SPAA\u201904, pp. 206\u2013215 (2004)","DOI":"10.1145\/1007912.1007944"},{"key":"19_CR8","unstructured":"Hendricks, J.: Efficient Byzantine Fault Tolerance for Scalable Storage and Services. Ph.D. thesis, Carnegie Mellon University, July 2009"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","DOI":"10.1145\/78969.78972"},{"issue":"OOPSLA1","key":"19_CR10","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1145\/3649826","volume":"8","author":"W Honor\u00e9","year":"2024","unstructured":"Honor\u00e9, W., Qiu, L., Kim, Y., Shin, J., Kim, J., Shao, Z.: Adob: bridging benign and byzantine consensus with atomic distributed objects. Proc. ACM Program. Lang. 8(OOPSLA1), 419\u2013448 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","DOI":"10.1145\/69575.69577"},{"key":"19_CR12","unstructured":"Kowalski, V., Most\u00e9faoui, A., Perrin, M.: Atomic register abstractions for byzantine-prone distributed systems. In: Bessani, A., D\u00e9fago, X., Nakamura, J., Wada, K., Yamauchi, Y. (eds.) 27th International Conference on Principles of Distributed Systems (OPODIS 2023), vol. 286, pp. 35:1\u201335:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Kshemkalyani, A.D., Piduguralla, M., Peri, S., Misra, A.: On constructing a byzantine linearizable swmr atomic register from swsr atomic registers. In: Proceedings of the 26th International Conference on Distributed Computing and Networking, pp. 239\u2013243. ICDCN \u201925. Association for Computing Machinery, New York (2025)","DOI":"10.1145\/3700838.3700839"},{"key":"19_CR14","unstructured":"Kuang, Y., Liang, H., Feng, X.: A program logic for byzantine-fault-tolerant protocols. Tech. rep. (2025). https:\/\/plax-lab.github.io\/publications\/byzlin\/setta25-tr.pdf"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, pp. 459\u2013470. Association for Computing Machinery, New York (2013)","DOI":"10.1145\/2491956.2462189"},{"key":"19_CR16","unstructured":"Liskov, B., Rodrigues, R.: Tolerating byzantine faulty clients in a quorum system. In: Proceedings of the 26th IEEE International Conference on Distributed Computing Systems (ICDCS 2006). IEEE Computer Society (2006)"},{"key":"19_CR17","unstructured":"Losa, G., Dodds, M.: On the formal verification of the stellar consensus protocol. In: Bernardo, B., Marmsoler, D. (eds.) 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), vol. 84, pp. 9:1\u20139:9. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995)","DOI":"10.1006\/inco.1995.1134"},{"key":"19_CR19","unstructured":"Malkhi, D., Reiter, M., Lynch, N.: A correctness condition for memory shared by byzantine processes. Unpublished manuscript, Sept 98 (1998)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Qiu, L., Kim, Y., Shin, J., Kim, J., Honor\u00e9, W., Shao, Z.: Lido: linearizable byzantine distributed objects with refinement-based liveness proofs. Proc. ACM Program. Lang. 8(PLDI), 1140\u20131164 (2024)","DOI":"10.1145\/3656423"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Rahli, V., Vukotic, I., V\u00f6lp, M., Esteves-Verissimo, P.: Velisarios: byzantine fault-tolerant protocols powered by coq. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 619\u2013650. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_22","DOI":"10.1007\/978-3-319-89884-1_22"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Toueg, S.: Randomized byzantine agreements. In: Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, PODC \u201984, pp. 163\u2013178. Association for Computing Machinery, New York (1984)","DOI":"10.1145\/800222.806744"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL, pp. 343\u2013356. ACM (2013)","DOI":"10.1145\/2429069.2429111"},{"key":"19_CR24","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, Computer Laboratory, July 2008. http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-726.pdf"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Zhao, Q., P\u00eerlea, G., Grzeszkiewicz, K., Gilbert, S., Sergey, I.: Compositional verification of composite byzantine protocols. In: Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, CCS\u201924, pp. 34\u201348. Association for Computing Machinery, New York (2024)","DOI":"10.1145\/3658644.3690355"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-7826-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T22:28:24Z","timestamp":1777847304000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-7826-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819578252","9789819578269"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-7826-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"1 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.setta2025.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}