pith. sign in

arxiv: 2604.03539 · v2 · pith:CD45XCC7new · submitted 2026-04-04 · 💻 cs.NI · cs.LO

CB-VER: A Stable Foundation for Modular Control Plane Verification

Dexin Zhang , Timothy Alberdingk Thijm , David Walker , Aarti Gupta This is my paper

Pith reviewed 2026-05-21 09:40 UTC · model grok-4.3

classification 💻 cs.NI cs.LO
keywords network control plane verificationeventually-stable propertiesconverges-before graphmodular verificationSMT solvingLean theorem proverfault tolerance
0
0 comments X

The pith

CB-Ver verifies eventually-stable network properties when a synthesized converges-before graph connects every component.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents CB-Ver as a framework for checking properties such as reachability or access control that hold in a network control plane after it stabilizes and continue to hold thereafter. Users supply interfaces describing each component's behavior, and the tool verifies local requirements for those interfaces using an SMT solver in parallel. It then builds a converges-before graph automatically and accepts the interfaces if the graph reaches every node, which also supports checking fault tolerance. The entire procedure is formalized and shown sound inside the Lean proof assistant.

Core claim

When a user provides interfaces for each network component, CB-Ver checks the necessary component-by-component requirements in parallel using an SMT solver. In addition, the tool automatically synthesizes a CB-graph and checks whether it connects all nodes in a network -- if it does, the interfaces are valid and users can check whether additional eventually-stable properties are implied. Moreover, the CB-graph can then be used to determine fault tolerance properties of the network. The verification algorithm is formalized and proved sound in Lean.

What carries the argument

The converges-before graph (CB-graph), a synthesized structure whose connectivity across all nodes certifies that the component interfaces imply the desired eventually-stable properties for the network as a whole.

If this is right

  • Component interfaces can be checked independently and in parallel before the global CB-graph test.
  • Once a valid CB-graph exists, fault-tolerance properties follow directly from the same structure.
  • Given a target CB-graph, a Constrained Horn Clause solver can synthesize the required interfaces automatically.
  • The soundness proof in Lean guarantees that any accepted interfaces truly imply the stated properties.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same CB-graph technique could be tried on stability questions in distributed systems that are not networks.
  • Automatic synthesis of interfaces might lower the barrier for operators who lack formal verification expertise.
  • Because the method separates local checks from the global connectivity test, it may scale to larger topologies than monolithic verifiers.

Load-bearing premise

That connectivity of the synthesized CB-graph is enough to guarantee the supplied interfaces imply the target eventually-stable properties throughout the network.

What would settle it

A concrete network and set of interfaces where the synthesized CB-graph connects every node yet some eventually-stable property fails to hold after the control plane converges.

Figures

Figures reproduced from arXiv: 2604.03539 by Aarti Gupta, David Walker, Dexin Zhang, Timothy Alberdingk Thijm.

Figure 1
Figure 1. Figure 1: Example network with devices A, B, C, D. A origi [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Synthesized CB-graphs for interfaces I1,Q1 and I2,Q2. route in Q2(C), and transfers this route to node E. Suppose E does not have any route before this transfer, e.g., if the route transfer from node B is much delayed. Then, as a result of transfer from C, node E will select this route where the path includes C. However, this route does not belong to Q2(E), as defined earlier (since its path includes C). T… view at source ↗
Figure 3
Figure 3. Figure 3: Summary: Verification Condition (VC) Formulas. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: CB-graph of a cross-world network from the Batfish [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: CHC system for the network interface synthesis problem, given the CB-graph. [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Evaluation results for CB-VER on fattree networks, compared with Timepiece (a modular verifier) and MS (a Minesweeper-style monolithic verifier). Internet2. CB-VER spends 22s (seconds) to verify the BlockToExternal property and reports 3 (true) violations (in phase 1). CB-VER spends 121s to verify the NoMartians property and reports one violation. Finally, CB-VER spends 74s successfully verifying InternalR… view at source ↗
Figure 7
Figure 7. Figure 7: Evaluation results for automated interface synthesis (CB-2IQ), compared with a monolithic verifier (MS). [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Debugging and Repair Process: Counterexample shows the VC violation in the first column, “ [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Topology of a campus network taken from the Bat [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Error debugging process: an example (for the network in Fig. [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗
read the original abstract

Network operators are often interested in verifying \emph{eventually-stable properties} of network control planes: properties of control plane states that hold eventually, and hold forever thereafter, provided the operating environment remains unchanged. Examples include eventually-stable reachability, access control, or path length properties. In this work, we introduce \textsc{CB-Ver}, a new framework for verifying such properties, based on the key idea of a \emph{converges-before graph} (CB-graph for short). When a user provides interfaces for each network component, \textsc{CB-Ver} checks the necessary component-by-component requirements in parallel using an SMT solver. In addition, the tool automatically synthesizes a CB-graph and checks whether it connects all nodes in a network -- if it does, the interfaces are valid and users can check whether additional eventually-stable properties are implied. Moreover, the CB-graph can then be used to determine fault tolerance properties of the network. We formalize our verification algorithm in the Lean theorem proving environment and prove its soundness. We evaluate the performance of \textsc{CB-Ver} on a range of benchmarks that demonstrate its ability to verify expressive properties in reasonable time. Finally, we demonstrate it is possible to automatically generate suitable interfaces by turning the problem around: Given a CB-graph, we use an off-the-shelf Constrained Horn Clause (CHC) solver to synthesize interfaces for every network component that together ensure the given correctness property.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper presents CB-Ver, a framework for verifying eventually-stable properties (e.g., reachability, access control) of network control planes. Users supply per-component interfaces that are checked in parallel via SMT; the tool synthesizes a converges-before graph (CB-graph) and accepts the interfaces if the graph is connected, after which additional properties and fault-tolerance claims can be checked. The verification algorithm, including the CB-graph connectivity implication, is formalized and proved sound in Lean. The paper also demonstrates automatic interface synthesis via an off-the-shelf CHC solver and reports performance on a range of benchmarks.

Significance. If the central claims hold, the work supplies a modular, formally grounded method for eventually-stable control-plane verification that scales via parallel SMT checks and automatic synthesis. The machine-checked Lean soundness proof is a clear strength, providing independent evidence that CB-graph connectivity implies interface validity under the stated assumptions. The CHC-based synthesis direction further increases practicality for operators.

major comments (1)
  1. §3 (Verification Procedure): the central claim that CB-graph connectivity is sufficient to guarantee that the supplied interfaces imply the target eventually-stable properties for the whole network is load-bearing; while the Lean formalization is cited, the manuscript should include a high-level statement of the key lemma (e.g., Lemma X) that directly links connectivity to validity so readers can assess the proof structure without inspecting the full Lean development.
minor comments (3)
  1. Abstract and §2: the term 'eventually-stable' is used inconsistently with respect to hyphenation and capitalization; standardize throughout.
  2. Evaluation section: timing results are reported but the hardware platform, solver versions, and exact network topologies used in the benchmarks are not specified, hindering reproducibility.
  3. Related-work discussion: a direct comparison table with prior modular or compositional verification tools (e.g., those using assume-guarantee or interface-based methods) would clarify the precise advance over existing approaches.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their constructive feedback and positive assessment of the work. We address the single major comment below and will incorporate the suggested change in the revised manuscript.

read point-by-point responses

  1. Referee: §3 (Verification Procedure): the central claim that CB-graph connectivity is sufficient to guarantee that the supplied interfaces imply the target eventually-stable properties for the whole network is load-bearing; while the Lean formalization is cited, the manuscript should include a high-level statement of the key lemma (e.g., Lemma X) that directly links connectivity to validity so readers can assess the proof structure without inspecting the full Lean development.

    Authors: We agree that a high-level statement of the key lemma would improve accessibility. In the revised version of §3, we will explicitly state the central lemma (Lemma 3.2) establishing that CB-graph connectivity implies interface validity for the composed network, i.e., that if the synthesized CB-graph is connected then the per-component interfaces together entail the target eventually-stable properties. This statement will be accompanied by a brief informal sketch of its role in the soundness argument, while the full machine-checked proof remains in the Lean development. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's core claim is that CB-graph connectivity (after SMT-based interface checks) suffices to validate supplied interfaces for eventually-stable network properties, with the full algorithm including this implication formalized and proved sound in Lean. A machine-checked proof in Lean constitutes independent evidence under the review criteria and does not reduce the result to a self-definitional or fitted-input construct. External SMT and CHC solvers are used for parallel checks and synthesis, keeping the derivation self-contained against external benchmarks rather than internally circular.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on the correctness of the CB-graph synthesis procedure and the assumption that user-supplied interfaces can be checked locally; the Lean proof is the primary external grounding.

axioms (1)
  • domain assumption Standard graph connectivity implies global eventual stability once local interface conditions hold
    Invoked when the paper states that a connecting CB-graph validates the interfaces.
invented entities (1)
  • Converges-before graph (CB-graph) no independent evidence
    purpose: To encode ordering constraints among component stabilizations so that global eventual stability can be checked via connectivity
    Newly introduced as the central modeling device; no independent evidence outside the paper is supplied in the abstract.

pith-pipeline@v0.9.0 · 5797 in / 1346 out tokens · 42083 ms · 2026-05-21T09:40:37.061361+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

50 extracted references · 50 canonical work pages

  1. [1]

    Internet2.https://internet2.edu, 2013

    work page 2013

  2. [2]

    https: //en.wikipedia.org/wiki/2022_Rogers_ Communications_outage

    2022 rogers communications outage. https: //en.wikipedia.org/wiki/2022_Rogers_ Communications_outage

    work page 2022

  3. [3]

    Tiramisu: Fast multilayer network verification

    Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. Tiramisu: Fast multilayer network verification. In17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 201–219, 2020

    work page 2020

  4. [4]

    A scalable, commodity data center network ar- chitecture.ACM SIGCOMM computer communication review, 38(4):63–74, 2008

    Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. A scalable, commodity data center network ar- chitecture.ACM SIGCOMM computer communication review, 38(4):63–74, 2008

    work page 2008

  5. [5]

    Kirigami, the verifiable art of net- work cutting

    Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Kirigami, the verifiable art of net- work cutting. In2022 IEEE 30th International Confer- ence on Network Protocols (ICNP), pages 1–12, 2022. 12

    work page 2022

  6. [6]

    modular control plane verification via temporal invariants

    Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Artifact associated with the pldi 2023 submission "modular control plane verification via temporal invariants"., 2023

    work page 2023

  7. [7]

    Modular control plane verification via temporal invariants.Proceedings of the ACM on Programming Languages, 7(PLDI):50–75, 2023

    Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, and David Walker. Modular control plane verification via temporal invariants.Proceedings of the ACM on Programming Languages, 7(PLDI):50–75, 2023

    work page 2023

  8. [8]

    PhD thesis, Princeton University, 2024

    Timothy Robin Alberdingk Thijm.Modular Control Plane Verification. PhD thesis, Princeton University, 2024

    work page 2024

  9. [9]

    Syntax-guided synthesis

    Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In2013 Formal Methods in Computer-Aided Design, pages 1–8. IEEE, 2013

    work page 2013

  10. [10]

    cvc5: A versatile and industrial-strength smt solver

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mo- hamed, Mudathir Mohamed, Aina Niemetz, Andres Nöt- zli, et al. cvc5: A versatile and industrial-strength smt solver. InInternational Conference on Tools and Al- gorithms for the Construction and Analysis of Systems, pages 415–442. Springer, 2022

    work page 2022

  11. [11]

    The Satisfiability Modulo Theories Library (SMT-LIB)

    Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016

    work page 2016

  12. [12]

    The smt-lib standard: Version 2.0

    Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. InProceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010

    work page 2010

  13. [13]

    A general approach to network configuration verification

    Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. A general approach to network configuration verification. InProceedings of the Conference of the ACM Special Interest Group on Data Communication, pages 155–168, 2017

    work page 2017

  14. [14]

    Control plane compression

    Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Control plane compression. InProceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 476–489, 2018

    work page 2018

  15. [15]

    Abstract interpretation of distributed network control planes.Proceedings of the ACM on Program- ming Languages, 4(POPL):1–27, 2019

    Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. Abstract interpretation of distributed network control planes.Proceedings of the ACM on Program- ming Languages, 4(POPL):1–27, 2019

    work page 2019

  16. [16]

    Bjørner, Arie Gurfinkel, Kenneth L

    Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMil- lan, and Andrey Rybalchenko. Horn clause solvers for program verification. InFields of Logic and Compu- tation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, volume 9300 ofLec- ture Notes in Computer Science, pages 24–51. Springer, 2015

    work page 2015

  17. [17]

    Lessons from the evolution of the batfish configuration analy- sis tool

    Matt Brown, Ari Fogel, Daniel Halperin, Victor Heo- rhiadi, Ratul Mahajan, and Todd Millstein. Lessons from the evolution of the batfish configuration analy- sis tool. InProceedings of the ACM SIGCOMM 2023 Conference, pages 122–135, 2023

    work page 2023

  18. [18]

    Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith

    Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstrac- tion refinement. InCAV, pages 154–169, 2000

    work page 2000

  19. [19]

    Asynchronous convergence of policy-rich distributed bellman-ford routing protocols

    Matthew L Daggitt, Alexander JT Gurney, and Timo- thy G Griffin. Asynchronous convergence of policy-rich distributed bellman-ford routing protocols. InProceed- ings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pages 103–116, 2018

    work page 2018

  20. [20]

    Z3: An effi- cient smt solver

    Leonardo De Moura and Nikolaj Bjørner. Z3: An effi- cient smt solver. InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008

    work page 2008

  21. [21]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2006

    Yefim Dinitz.Dinitz’ Algorithm: The Original Version and Even’s Version, pages 218–240. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006

    work page 2006

  22. [22]

    A general approach to network configuration analysis

    Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed- Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. A general approach to network configuration analysis. In12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 469–483, 2015

    work page 2015

  23. [23]

    Fast control plane analysis using an abstract representation

    Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. Fast control plane analysis using an abstract representation. InProceedings of the 2016 ACM SIGCOMM Conference, pages 300–313, 2016

    work page 2016

  24. [24]

    Lopes, Corneliu Popeea, and Andrey Rybalchenko

    Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing soft- ware verifiers from proof rules. InACM SIGPLAN Conference on Programming Language Design and Im- plementation, PLDI, pages 405–416. ACM, 2012

    work page 2012

  25. [25]

    The stable paths problem and interdomain routing

    Timothy G Griffin, F Bruce Shepherd, and Gordon Wil- fong. The stable paths problem and interdomain routing. IEEE/ACM Transactions On Networking, 10(2):232– 243, 2002

    work page 2002

  26. [26]

    Metarouting

    Timothy G Griffin and Joäo Luís Sobrinho. Metarouting. InProceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications, pages 1–12, 2005. 13

    work page 2005

  27. [27]

    Validating datacenters at scale,

    Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. Validating datacenters at scale,

    work page

  28. [28]

    Presentation at SIGCOMM 2019

    work page 2019

  29. [29]

    Validating datacenters at scale

    Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. Validating datacenters at scale. InProceedings of the ACM Special Interest Group...

    work page 2019

  30. [30]

    Header space analysis: Static checking for net- works

    Peyman Kazemian, George Varghese, and Nick McK- eown. Header space analysis: Static checking for net- works. In9th USENIX Symposium on Networked Sys- tems Design and Implementation (NSDI 12), pages 113– 126, 2012

    work page 2012

  31. [31]

    Veriflow: Verifying network-wide invariants in real time

    Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. Veriflow: Verifying network-wide invariants in real time. InProceedings of the first work- shop on Hot topics in software defined networks, pages 49–54, 2012

    work page 2012

  32. [32]

    Smt-based model checking for recursive programs

    Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. Smt-based model checking for recursive programs. In Armin Biere and Roderick Bloem, editors,Computer Aided Verification, pages 17–34, Cham, 2014. Springer International Publishing

    work page 2014

  33. [33]

    Smt-based model checking for recursive programs.For- mal Methods in System Design, 48(3):175–205, 2016

    Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. Smt-based model checking for recursive programs.For- mal Methods in System Design, 48(3):175–205, 2016

    work page 2016

  34. [34]

    Time, clocks, and the ordering of events in a distributed system

    Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. InConcurrency: the Works of Leslie Lamport, pages 179–196. 2019

    work page 2019

  35. [35]

    Checking beliefs in dynamic networks

    Nuno P Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. Checking beliefs in dynamic networks. In12th USENIX Sympo- sium on Networked Systems Design and Implementation (NSDI 15), pages 499–512, 2015

    work page 2015

  36. [36]

    Debugging the data plane with anteater

    Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P Brighten Godfrey, and Samuel Tal- madge King. Debugging the data plane with anteater. ACM SIGCOMM Computer Communication Review, 41(4):290–301, 2011

    work page 2011

  37. [37]

    Microsoft. Zen. https://github.com/ microsoft/Zen/tree/master

    work page

  38. [38]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. InAu- tomated Deduction–CADE 28: 28th International Con- ference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021

    work page 2021

  39. [39]

    Plankton: Scal- able network configuration verification through model checking

    Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. Plankton: Scal- able network configuration verification through model checking. In17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 953–967, 2020

    work page 2020

  40. [40]

    Acorn: Network control plane abstraction using route nondeterminism

    Divya Raghunathan, Ryan Beckett, Aarti Gupta, and David Walker. Acorn: Network control plane abstraction using route nondeterminism. InFMCAD, pages 261– 272, 2022

    work page 2022

  41. [41]

    An algebraic theory of dynamic net- work routing.IEEE/ACM Transactions on Networking, 13(5):1160–1173, 2005

    Joao L Sobrinho. An algebraic theory of dynamic net- work routing.IEEE/ACM Transactions on Networking, 13(5):1160–1173, 2005

    work page 2005

  42. [42]

    Lightyear: Using modularity to scale bgp control plane verification

    Alan Tang, Ryan Beckett, Steven Benaloh, Karthick Ja- yaraman, Tejas Patil, Todd Millstein, and George Vargh- ese. Lightyear: Using modularity to scale bgp control plane verification. InProceedings of the ACM SIG- COMM 2023 Conference, pages 94–107, 2023

    work page 2023

  43. [43]

    Parallel asynchronous algorithms for discrete data.Journal of the ACM (JACM), 37(3):588–606, 1990

    Aydin Üresin and Michel Dubois. Parallel asynchronous algorithms for discrete data.Journal of the ACM (JACM), 37(3):588–606, 1990

    work page 1990

  44. [44]

    Introduction to route computation and analysis using batfish

    Harsh Verma and Dan Halperin. Introduction to route computation and analysis using batfish. https: //github.com/batfish/pybatfish/blob/ master/jupyter_notebooks/Introduction% 20to%20Route%20Analysis.ipynb, August 2018

    work page 2018

  45. [45]

    Expresso: Comprehensively reasoning about external routes using symbolic simulation

    Dan Wang, Peng Zhang, and Aaron Gember-Jacobson. Expresso: Comprehensively reasoning about external routes using symbolic simulation. InProceedings of the ACM SIGCOMM Conference, pages 197–212. ACM, 2024

    work page 2024

  46. [46]

    Scalable verification of border gateway protocol con- figurations with an smt solver

    Konstantin Weitz, Doug Woos, Emina Torlak, Michael D Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Scalable verification of border gateway protocol con- figurations with an smt solver. InProceedings of the 2016 acm sigplan international conference on object- oriented programming, systems, languages, and appli- cations, pages 765–780, 2016. 14

    work page 2016

  47. [47]

    Accuracy, scalability, coverage: A practical configuration verifier on a global wan

    Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, et al. Accuracy, scalability, coverage: A practical configuration verifier on a global wan. InProceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, archite...

    work page 2020

  48. [48]

    sv ✓” in the second column indicates the user’s belief that routesv is aplausibleroute that be selected by v, and “sv ✗

    Yifei Yuan. Analyzing the impact of failures (and letting loose a chaos monkey). https://github.com/ batfish/pybatfish/blob/master/jupyter_ notebooks/Analyzing%20the%20Impact%20of% 20Failures%20(and%20letting%20loose%20a% 20Chaos%20Monkey).ipynb, December 2018. A Repository for Lean formalization and benchmarks The benchmarks are presented in https://gith...

    work page 2018

  49. [49]

    The local preference of routes are the same as the default value (100), so that longer paths do not have higher local preference to be selected

    work page

  50. [50]

    down” link (core to aggregation or aggregation to edge), a community tag 1:0 will be added. • Routes with community tag 1:0 will be dropped along “up

    Before convergence, the router may select another route, but the length must not be less than the distance dist(v). Therefore, the interfaces forPathLengthare I(v) ={s|s=∞⇒lp(s) =100∧len(s)≥dist(v)} Q(v) ={s|s̸=∞∧lp(s) =100∧len(s) =dist(v)} Valley-free.In ValleyFree we check the valley-free prop- erty in fattrees, i.e., no valley path (up-down-up path) is...

    work page