@inproceedings{867401e52a304ce8a11fe250e3911082,
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 “at least as good.” 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–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",
}