To refer to this page use:
|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.|
|Citation:||Giannarakis, Nick, Ryan Beckett, Ratul Mahajan, and David Walker. "Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement." In International Conference on Computer Aided Verification (2019): pp. 305-323. doi:10.1007/978-3-030-25543-5_18|
|Pages:||305 - 323|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Conference on Computer Aided Verification|
|Version:||Final published version. This is an open access article.|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.