@inproceedings{a3ca4f30caed4b758dc73b87be17779e,
title = "Fast SMT-Based Fault Tolerance Verification for Wide Area Networks",
abstract = "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 k links fail, a verifier needs to explore a tremendous space of failure scenarios. To this end, this paper proposes VeriBoost, 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. VeriBoost 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{\textendash}47{\texttimes}.",
keywords = "Failures, SMT, Verification, Wide Area Network",
author = "Ning Kang and Peng Zhang and Hao Li and Jianyuan Zhang",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2026.; 27th International Symposium on Formal Methods, FM 2026 ; Conference date: 18-05-2026 Through 22-05-2026",
year = "2026",
doi = "10.1007/978-3-032-26220-2\_7",
language = "英语",
isbn = "9783032262196",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "133--153",
editor = "Augusto Sampaio and Marielle Stoelinga",
booktitle = "Formal Methods - 27th International Symposium, FM 2026, Proceedings",
}