{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:50Z","timestamp":1783545350830,"version":"3.55.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Configurations of routing protocols in wide area networks (WANs) are highly sophisticated and prone to bugs, leading to severe network outages and security breaches. SMT-based network verification can assist operators in checking the configurations, but it still faces scalability challenges when reasoning about failures: to check whether a property holds when no more than\n                    <jats:italic>k<\/jats:italic>\n                    links fail, a verifier needs to explore a tremendous space of failure scenarios. To this end, this paper proposes\n                    <jats:italic>VeriBoost<\/jats:italic>\n                    , a method that can leverage the topology features of WANs to reduce the space of failure scenarios, thereby improving the scalability of SMT-based verification on WANs.\n                    <jats:italic>VeriBoost<\/jats:italic>\n                    achieves the reduction by pruning links that are irrelevant to a property, and compressing multiple links whose failures have an equivalent impact on the property. Experiments on real WAN topologies show that it speeds up SMT-based verification by 2\u201347\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\times $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>\u00d7<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_7","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:20:32Z","timestamp":1779024032000},"page":"133-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fast SMT-Based Fault Tolerance Verification for\u00a0Wide Area Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3977-5093","authenticated-orcid":false,"given":"Ning","family":"Kang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7721-2675","authenticated-orcid":false,"given":"Peng","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8776-6911","authenticated-orcid":false,"given":"Hao","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9892-9244","authenticated-orcid":false,"given":"Jianyuan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Abhashkumar, A., Gember-Jacobson, A., Akella, A.: Tiramisu: fast multilayer network verification. In: 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2020), pp. 201\u2013219 (2020). https:\/\/doi.org\/10.23919\/ifipnetworking55013.2022.9829765","DOI":"10.23919\/ifipnetworking55013.2022.9829765"},{"issue":"4","key":"7_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1402958.1402967","volume":"38","author":"M Al-Fares","year":"2008","unstructured":"Al-Fares, M., Loukissas, A., Vahdat, A.: A scalable, commodity data center network architecture. ACM SIGCOMM Comput. Commun. Rev. 38(4), 63\u201374 (2008). https:\/\/doi.org\/10.1145\/1402958.1402967","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Alberdingk\u00a0Thijm, T., Beckett, R., Gupta, A., Walker, D.: Modular control plane verification via temporal invariants. Proc. ACM Program. Lang. 7(PLDI), 50\u201375 (2023). https:\/\/doi.org\/10.1145\/3591222","DOI":"10.1145\/3591222"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication, pp. 155\u2013168 (2017). https:\/\/doi.org\/10.1145\/3098822.3098834","DOI":"10.1145\/3098822.3098834"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Beckett, R., Gupta, A., Mahajan, R., Walker, D.: Control plane compression. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 476\u2013489 (2018). https:\/\/doi.org\/10.1145\/3230543.3230583","DOI":"10.1145\/3230543.3230583"},{"key":"7_CR6","unstructured":"Birkner, R., Drachsler-Cohen, D., Vanbever, L., Vechev, M.: Config2spec: mining network specifications from network configurations. In: 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2020), pp. 969\u2013984 (2020)"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Brown, M., Fogel, A., Halperin, D., Heorhiadi, V., Mahajan, R., Millstein, T.: Lessons from the evolution of the batfish configuration analysis tool. In: Proceedings of the ACM SIGCOMM 2023 Conference, pp. 122\u2013135 (2023). https:\/\/doi.org\/10.1145\/3603269.3604866","DOI":"10.1145\/3603269.3604866"},{"key":"7_CR8","unstructured":"Brown, M., Fogel, A., Halperin, D., Heorhiadi, V., Mahajan, R., Millstein, T.: The open-source code of batfish (2023). https:\/\/github.com\/batfish\/batfish"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Diestel, R.: Graph Theory. Springer (print edition); Reinhard Diestel (eBooks) (2024). https:\/\/doi.org\/10.1007\/978-3-662-53622-3","DOI":"10.1007\/978-3-662-53622-3"},{"key":"7_CR11","unstructured":"El-Hassany, A., Tsankov, P., Vanbever, L., Vechev, M.: Netcomplete: practical $$\\{$$Network-Wide$$\\}$$ configuration synthesis with autocompletion. In: 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2018), pp. 579\u2013594 (2018)"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Fang, X., et al.: Network can help check itself: accelerating SMT-based network configuration verification using network domain knowledge. In: IEEE\/International Conference on Computer (2023). https:\/\/doi.org\/10.1109\/infocom52122.2024.10621215","DOI":"10.1109\/infocom52122.2024.10621215"},{"issue":"2","key":"7_CR13","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1109\/tnet.2007.892876","volume":"15","author":"N Feamster","year":"2007","unstructured":"Feamster, N., Rexford, J.: Network-wide prediction of BGP routes. IEEE\/ACM Trans. Networking 15(2), 253\u2013266 (2007). https:\/\/doi.org\/10.1109\/tnet.2007.892876","journal-title":"IEEE\/ACM Trans. Networking"},{"key":"7_CR14","unstructured":"Fogel, A., et al.: A general approach to network configuration analysis. In: 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2015), pp. 469\u2013483 (2015)"},{"issue":"6","key":"7_CR15","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1145\/345063.339426","volume":"9","author":"L Gao","year":"2001","unstructured":"Gao, L., Rexford, J.: Stable internet routing without global coordination. IEEE\/ACM Trans. Networking 9(6), 681\u2013692 (2001). https:\/\/doi.org\/10.1145\/345063.339426","journal-title":"IEEE\/ACM Trans. Networking"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-030-25543-5_18","volume-title":"Computer Aided Verification","author":"N Giannarakis","year":"2019","unstructured":"Giannarakis, N., Beckett, R., Mahajan, R., Walker, D.: Efficient verification of network fault tolerance via counterexample-guided refinement. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 305\u2013323. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_18"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Harary, F.: Graph Theory (on Demand Printing of 02787). CRC Press (2018). https:\/\/doi.org\/10.1201\/9780429493768","DOI":"10.1201\/9780429493768"},{"key":"7_CR18","unstructured":"Kang, N.: The appendix of veriboost (2026). https:\/\/xjtu-netverify.github.io\/papers\/VeriBoost\/veriboost_final_version.pdf"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Kang, N., Zhang, P., Li, H., Wen, S., Ji, C., Yang, Y.: Network specification mining with high fidelity and scalability. In: 2023 IEEE 31st International Conference on Network Protocols (ICNP), pp. 1\u201311. IEEE (2023). https:\/\/doi.org\/10.1109\/icnp59255.2023.10355598","DOI":"10.1109\/icnp59255.2023.10355598"},{"issue":"9","key":"7_CR20","doi-asserted-by":"publisher","first-page":"1765","DOI":"10.1109\/jsac.2011.111002","volume":"29","author":"S Knight","year":"2011","unstructured":"Knight, S., Nguyen, H.X., Falkner, N., Bowden, R., Roughan, M.: The internet topology zoo. IEEE J. Sel. Areas Commun. 29(9), 1765\u20131775 (2011). https:\/\/doi.org\/10.1109\/jsac.2011.111002","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Liu, Y., Subotic, P., Letier, E., Mechtaev, S., Roychoudhury, A.: Efficient SMT-based network fault tolerance verification. In: International Symposium on Formal Methods, pp. 92\u2013100. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_7","DOI":"10.1007\/978-3-031-27481-7_7"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-030-11245-5_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"NP Lopes","year":"2019","unstructured":"Lopes, N.P., Rybalchenko, A.: Fast BGP simulation of large datacenters. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 386\u2013408. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_18"},{"key":"7_CR23","unstructured":"Moss, S.: Microsoft azure outage blamed on wan router IP change (2023). https:\/\/www.datacenterdynamics.com\/en\/news\/microsoft-azure-outage-blamed-on-wan-router-ip-change\/"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Raghunathan, D., Beckett, R., Gupta, A., Walker, D.: Acorn: network control plane abstraction using route nondeterminism. In: FMCAD, pp. 261\u2013272 (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_33","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_33"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Rekhter, Y., Li, T., Hares, S.: RFC 4271: a border gateway protocol 4 (BGP-4) (2006). https:\/\/doi.org\/10.17487\/rfc4271","DOI":"10.17487\/rfc4271"},{"issue":"6","key":"7_CR26","doi-asserted-by":"publisher","first-page":"2493","DOI":"10.1109\/tnet.2022.3176267","volume":"30","author":"X Shao","year":"2022","unstructured":"Shao, X., Chen, Z., Holcomb, D., Gao, L.: Accelerating BGP configuration verification through reducing cycles in SMT constraints. IEEE\/ACM Trans. Networking 30(6), 2493\u20132504 (2022). https:\/\/doi.org\/10.1109\/tnet.2022.3176267","journal-title":"IEEE\/ACM Trans. Networking"},{"key":"7_CR27","unstructured":"Sharwood, S.: Facebook rendered spineless by buggy audit code that missed catastrophic network config error (2021). https:\/\/www.theregister.com\/2021\/10\/06\/facebook_outage_explained_in_detail\/"},{"issue":"5","key":"7_CR28","doi-asserted-by":"publisher","first-page":"1160","DOI":"10.1109\/tnet.2005.857111","volume":"13","author":"JL Sobrinho","year":"2005","unstructured":"Sobrinho, J.L.: An algebraic theory of dynamic network routing. IEEE\/ACM Trans. Networking 13(5), 1160\u20131173 (2005). https:\/\/doi.org\/10.1109\/tnet.2005.857111","journal-title":"IEEE\/ACM Trans. Networking"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Steffen, S., Gehr, T., Tsankov, P., Vanbever, L., Vechev, M.: Probabilistic verification of network configurations. In: Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, pp. 750\u2013764 (2020). https:\/\/doi.org\/10.1145\/3387514.3405900","DOI":"10.1145\/3387514.3405900"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Tang, A., et al.: Lightyear: using modularity to scale BGP control plane verification. In: Proceedings of the ACM SIGCOMM 2023 Conference, pp. 94\u2013107 (2023). https:\/\/doi.org\/10.1145\/3603269.3604842","DOI":"10.1145\/3603269.3604842"},{"issue":"2","key":"7_CR31","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/swat.1971.10","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972). https:\/\/doi.org\/10.1109\/swat.1971.10","journal-title":"SIAM J. Comput."},{"key":"7_CR32","doi-asserted-by":"publisher","DOI":"10.1109\/tnet.2024.3360371","author":"TA Thijm","year":"2024","unstructured":"Thijm, T.A., Beckett, R., Gupta, A., Walker, D.: Kirigami, the verifiable art of network cutting. IEEE\/ACM Trans. Networking (2024). https:\/\/doi.org\/10.1109\/tnet.2024.3360371","journal-title":"IEEE\/ACM Trans. Networking"},{"key":"7_CR33","unstructured":"Tom\u00a0Strickx, J.H.: Cloudflare outage on June 21, 2022 (2022). https:\/\/blog.cloudflare.com\/cloudflare-outage-on-june-21-2022\/"},{"key":"7_CR34","volume-title":"Introduction to Graph Theory","author":"DB West","year":"2001","unstructured":"West, D.B.: Introduction to Graph Theory, vol. 2. Prentice Hall, Upper Saddle River (2001)"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Yang, R., Gao, R., Zhang, C.: A new algebraic approach to finding all simple paths and cycles in undirected graphs. In: 2015 IEEE International Conference on Information and Automation, pp. 1887\u20131892. IEEE (2015). https:\/\/doi.org\/10.1109\/icinfa.2015.7279596","DOI":"10.1109\/icinfa.2015.7279596"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"Ye, F., et al.: Accuracy, scalability, coverage: a practical configuration verifier on a global wan. In: Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, pp. 599\u2013614 (2020). https:\/\/doi.org\/10.1145\/3387514.3406217","DOI":"10.1145\/3387514.3406217"},{"key":"7_CR37","unstructured":"Zhang, P., Gember-Jacobson, A., Zuo, Y., Huang, Y., Liu, X., Li, H.: Differential network analysis. In: 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2022), pp. 601\u2013615 (2022)"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Zhang, P., Wang, D., Gember-Jacobson, A.: Symbolic router execution. In: Proceedings of the ACM SIGCOMM 2022 Conference, pp. 336\u2013349 (2022). https:\/\/doi.org\/10.1145\/3544216.3544264","DOI":"10.1145\/3544216.3544264"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:30:10Z","timestamp":1783542610000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_7","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}