@inproceedings{ce8275ca0ed742c5ac46dd0472ddc261,
title = "Efficient verification of network fault tolerance via counterexample-guided refinement",
abstract = "We show how to verify that large data center networks satisfy key properties such as all-pairs reachability under a bounded number of faults. To scale the analysis, we develop algorithms that identify network symmetries and compute small abstract networks from large concrete ones. Using counter-example guided abstraction refinement, we successively refine the computed abstractions until the given property may be verified. The soundness of our approach relies on a novel notion of network approximation: routing paths in the concrete network are not precisely simulated by those in the abstract network but are guaranteed to be {\textquotedblleft}at least as good.{\textquotedblright} We implement our algorithms in a tool called Origami and use them to verify reachability under faults for standard data center topologies. We find that Origami computes abstract networks with 1{\textendash}3 orders of magnitude fewer edges, which makes it possible to verify large networks that are out of reach of existing techniques.",
author = "Nick Giannarakis and Ryan Beckett and Ratul Mahajan and David Walker",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2019.; 31st International Conference on Computer Aided Verification, CAV 2019 ; Conference date: 15-07-2019 Through 18-07-2019",
year = "2019",
doi = "10.1007/978-3-030-25543-5\_18",
language = "English (US)",
isbn = "9783030255428",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "305--323",
editor = "Isil Dillig and Serdar Tasiran",
booktitle = "Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings",
address = "Germany",
}