Guided Exploration of Control Plane Routing States
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.
Research Areas: Network Analysis and Reasoning and Verification and Synthesis
People
BibTex
@inproceedings{schneider2025guided,
title={Guided Exploration of Control Plane Routing States},
author={Schneider, Tibor and Mégret, Jean Bernard David and Vanbever, Laurent},
booktitle={33rd IEEE International Conference on Network Protocols (ICNP 2025)},
year={2025}
}Research Collection: 20.500.11850/783996
Slide Sources: https://gitlab.ethz.ch/projects/57055