{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:04:18Z","timestamp":1781193858610,"version":"3.54.1"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","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-3-032-28079-4_1","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:30:32Z","timestamp":1781191832000},"page":"3-24","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Interactive Safety Verification of\u00a0Distributed Protocols by\u00a0Inductive Proof Decomposition"],"prefix":"10.1007","author":[{"given":"William","family":"Schultz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edward","family":"Ashton","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heidi","family":"Howard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"1_CR1","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media (2013)"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"1_CR3","unstructured":"Braithwaite, S., et al.: Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). In: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (2020)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A., Arvind: Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proceedings of ACM Programming Language 1, ICFP (2017)","DOI":"10.1145\/3110268"},{"key":"1_CR5","unstructured":"Corbett, J.C., et al.: Google\u2019s Globally-Distributed Database. In: OSDI, Spanner (2012)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA+ Proofs. In: Giannakopoulou, D., Mery, D. (eds.) Proceedings of the 18th International Symposium on Formal Methods (FM 2012), Lecture Notes in Computer Science, Vol. 7436, pp. 147\u2013154 (2012)","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"1_CR7","unstructured":"Dardik, I., Porter, A., Kang, E.: Recomposition: A new technique for efficient compositional verification. In: 2024 Formal Methods in Computer-Aided Design (FMCAD), pp.\u00a0130\u2013141 (2024)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: Giacobazzi, R., Cousot, R., (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23\u201325, 2013, pp.\u00a0129\u2013142, ACM (2013)","DOI":"10.1145\/2429069.2429086"},{"key":"1_CR9","first-page":"131","volume-title":"Methods: 13th International Symposium, NFM 2021, Virtual Event, May 24\u201328, 2021","author":"A Goel","year":"2021","unstructured":"Goel, A., Sakallah, K.: On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. In: Formal, N.A.S.A. (ed.) Methods: 13th International Symposium, NFM 2021, Virtual Event, May 24\u201328, 2021, pp. 131\u2013150. Springer-Verlag, Proceedings (Berlin, Heidelberg (2021)"},{"key":"1_CR10","unstructured":"Goel, A., Sakallah, K.A.: Towards an automatic proof of Lamport\u2019s Paxos. In: 2021 Formal Methods in Computer Aided Design (FMCAD), pp. 112\u2013122 (2021)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Gordon, M.J., Kaufmann, M., Ray, S.: The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4. J. Autom. Reason. 47(1), 1\u201316 (2011)","DOI":"10.1007\/s10817-010-9169-y"},{"key":"1_CR12","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: it\u2019s a small (enough) world after all. In: 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21), pp.\u00a0115\u2013131, USENIX Association (2021)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles (New York, NY, USA, 2015), SOSP \u201915, pp.\u00a01\u201317. Association for Computing Machinery, (2015)","DOI":"10.1145\/2815400.2815428"},{"issue":"5","key":"1_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Huang, D., et al.: TiDB: a raft-based HTAP database. Proc. VLDB Endow. 13(12), 3072\u20133084 (2020)","DOI":"10.14778\/3415478.3415535"},{"issue":"2104","key":"1_CR16","doi-asserted-by":"publisher","first-page":"20150399","DOI":"10.1098\/rsta.2015.0399","volume":"375","author":"WA Hunt Jr","year":"2017","unstructured":"Hunt, W.A., Jr., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with acl2. Philos. Trans. Royal Soc. A: Mat. Phys. Eng. Sci. 375(2104), 20150399 (2017)","journal-title":"Philos. Trans. Royal Soc. A: Mat. Phys. Eng. Sci."},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-33125-1_17","volume-title":"Static Analysis","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: Path-Sensitive Backward Slicing. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 231\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33125-1_17"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Path slicing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming language Design and Implementation, pp.\u00a038\u201347 (2005)","DOI":"10.1145\/1065010.1065016"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1) (2017)","DOI":"10.1145\/3022187"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Koenig, J.\u00a0R., Padon, O., Immerman, N., Aiken, A.: First-order quantified separators. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, p.\u00a0703\u2013717. PLDI 2020, Association for Computing Machinery (2020)","DOI":"10.1145\/3385412.3386018"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-030-99524-9_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JR Koenig","year":"2022","unstructured":"Koenig, J.R., Padon, O., Shoham, S., Aiken, A.: Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion. In: TACAS 2022. LNCS, vol. 13243, pp. 338\u2013356. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_18"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Konnov, I., Kukovec, J., Tran, T.-H.: TLA+ model checking made symbolic. Proceedings of ACM Programmming Language, vol. 3, OOPSLA (2019)","DOI":"10.1145\/3360549"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","DOI":"10.1145\/361082.361093"},{"issue":"7","key":"1_CR24","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1080\/00029890.1995.12004627","volume":"102","author":"L Lamport","year":"1995","unstructured":"Lamport, L.: How to write a proof. Am. Math. Mon. 102(7), 600\u2013608 (1995)","journal-title":"Am. Math. Mon."},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Paxos made simple. ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001), pp. 51\u201358 (2001)","DOI":"10.1145\/568425.568433"},{"key":"1_CR26","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"1_CR27","unstructured":"Lamport, L.: Using TLC to Check Inductive Invariance (2018). http:\/\/lamport.azurewebsites.net\/tla\/inductive-invariant.pdf"},{"key":"1_CR28","unstructured":"Lampson, B., Sturgis, H.: Crash recovery in a distributed data storage system. Unpublished technical report, Xerox Palo Alto Research Center (1979)"},{"key":"1_CR29","unstructured":"Ma, H., et al.: Sift: using refinement-guided automation to verify complex distributed systems. In: USENIX Annual Technical Conference (2022)"},{"key":"1_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer-Verlag, Berlin, Heidelberg (1995)"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Newcombe, C.: Why amazon chose TLA+. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp.\u00a025\u201339. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_3","DOI":"10.1007\/978-3-662-43652-3_3"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): : 5. The Rules of the Game. In: Isabelle\/HOL. LNCS, vol. 2283, pp. 67\u2013104. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9_5","DOI":"10.1007\/3-540-45949-9_5"},{"key":"1_CR33","unstructured":"Ongaro, D.: Consensus: bridging theory and practice. Doctoral thesis (2014)"},{"key":"1_CR34","unstructured":"Ongaro, D., Ousterhout, J.: In Search of an understandable consensus algorithm. In: Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USA, 2014), USENIX ATC\u201914, USENIX Association, pp.\u00a0305\u2013320 (2014)"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of Inferring Inductive Invariants. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.\u00a0217\u2013231 (New York, NY, USA), POPL \u201916, Association for Computing Machinery (2016)","DOI":"10.1145\/2837614.2837640"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.\u00a0614\u2013630. (New York, NY, USA), PLDI \u201916, Association for Computing Machiner (2016)","DOI":"10.1145\/2908080.2908118"},{"key":"1_CR37","unstructured":"Schultz, W.: Artifact for NFM 2026 paper: interactive safety verification of distributed protocols by inductive proof decomposition (2026). https:\/\/github.com\/will62794\/nfm26-artifact, Accessed 24 Mar 2026"},{"key":"1_CR38","unstructured":"Schultz, W.: Scimitar: verification tool for distributed protocols based on inductive proof decomposition (2026). https:\/\/github.com\/will62794\/scimitar, Accessed 24 Mar 2026"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Schultz, W., Dardik, I., Tripakis, S.: Formal verification of a distributed dynamic reconfiguration protocol. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 143\u2013152 (Philadelphia, PA, USA), CPP 2022, Association for Computing Machinery (2022)","DOI":"10.1145\/3497775.3503688"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Taft, R., et al.: CockroachDB: the resilient geo-distributed SQL database. In: Proceedings of the 2020 ACM SIGMOD International Conference on Management of Data, pp.\u00a01493\u20131509. SIGMOD \u201920, Association for Computing Machinery (2020)","DOI":"10.1145\/3318464.3386134"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Taube, M., et al.: Modularity for decidability of deductive verification with applications to distributed systems. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.\u00a0662\u2013677 (2018)","DOI":"10.1145\/3192366.3192414"},{"key":"1_CR42","unstructured":"Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3 (1994)"},{"key":"1_CR43","unstructured":"Vanlightly, J.: raft-tlaplus: a TLA+ specification of the Raft distributed consensus algorithm (2023). https:\/\/github.com\/Vanlightly\/raft-tlaplus\/blob\/main\/specifications\/standard-raft\/Raft.tla, GitHub repository"},{"key":"1_CR44","unstructured":"Wilcox, J.R.: Compositional and automated verification of distributed systems. PhD thesis, University of Washington, USA (2021)"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.\u00a0357\u2013368. Portland, OR, USA, June 15\u201317, 2015, ACM (2015)","DOI":"10.1145\/2737924.2737958"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.\u00a0R., Anton, S., Tatlock, Z., Ernst, M.\u00a0D., and Anderson, T. Planning for Change in a Formal Verification of the Raft Consensus Protocol. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.\u00a0154\u2013165. CPP 2016, Association for Computing Machinery (2016)","DOI":"10.1145\/2854065.2854081"},{"key":"1_CR47","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: fast, automated inference of inductive invariants for verifying distributed protocols. In: Aguilera, M.K., Weatherspoon, H. (eds.) 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, pp.\u00a0485\u2013501. Carlsbad, CA, USA, July 11\u201313, 2022 USENIX Association (2022)"},{"key":"1_CR48","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: DistAI: data-driven automated invariant learning for distributed protocols. In: 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21), pp.\u00a0405\u2013421. USENIX Association (2021)"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA+ Specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:30:52Z","timestamp":1781191852000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_1","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":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}