Guided Exploration of Control Plane Routing States
OPEN ACCESS
Loading...
Date
2025
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
In recent years, significant progress has been madetowards scalable network control-plane verification. Yet, opera-tors are still hesitant to deploy such systems. We argue that thisreluctance is in part due to a semantic gap between operatorsreasoning about routing states and verifiers exploring the spaceof environments. Indeed, operators express the specification interms of behavior of routing states, while verifiers usually rely onsolvers to find specific environments that violate the specification.This semantic gap prevents users from guiding these solvers todirectly explore routing states that violate the specification, or tosearch for states that are most relevant or likely.
In this paper, we present a new approach for flexible control-plane verification. Instead of relying on rigid off-the-shelf solvers,we design a novel backtracking algorithm to directly explore thespace of routing states. This enables users to guide the explorationaccording to the specification and domain-specific knowledgefrom operators. This algorithm paves the way for novel use cases,ranging from finding relevant (e.g., likely) counterexamples toperforming verification of probabilistic specifications.
Permanent link
Publication status
accepted
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
Event
33rd IEEE International Conference on Network Protocols (ICNP 2025)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Routing protocols; Formal verification
Organisational unit
09477 - Vanbever, Laurent / Vanbever, Laurent
Notes
Conference lecture held on September 24, 2025.
Funding
851809 - From Network Verification to Synthesis: Breaking New Ground in Network Automation (EC)