Open access
Date
2023-12-08Type
- Conference Paper
ETH Bibliography
yes
Altmetrics
Abstract
Control plane verification promises to help operators build reliable networks by reporting a counterexample that violates the specification. However, a single counterexample imposes a major challenge for operators to understand and repair the violation. To improve the usability of control plane verification, we present the first verifier computing the space of all specification violations as a symbolic expression. Our prototype implementation computes the causality between the network routing state and the external routing inputs that induce that state.
Describing the space of all violations helps operators address the
root cause of the violation, while presenting the space as a symbolic
expression allows operators to further manipulate the output to
inspect certain aspects of the problem. Show more
Permanent link
https://doi.org/10.3929/ethz-b-000643612Publication status
publishedExternal links
Book title
CoNEXT-SW '23: Proceedings of the on CoNEXT Student Workshop 2023Pages / Article No.
Publisher
Association for Computing MachineryEvent
Subject
Network verification; Control plane verification; Network analysisOrganisational unit
09477 - Vanbever, Laurent / Vanbever, Laurent
Funding
851809 - From Network Verification to Synthesis: Breaking New Ground in Network Automation (EC)
Notes
Conference lecture held on December 8, 2023.More
Show all metadata
ETH Bibliography
yes
Altmetrics