A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification

Alex Horn; Ali Kheradmand; Mukul R. Prasad

REVIEW 4 major objections 5 minor 90 references

A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims that its #PEC algorithm constructs the unique minimal packet equivalence classes without binary decision diagrams, by counting headers to detect empty classes, and does so faster than the BDD-based approach while…

desk verdict A genuine and mostly sound algorithmic contribution to network verification; the stress-test self-loop is a misreading, but the evaluation is under-powered and the proof for the DAG update is deferred. read the letter →

arxiv 1908.09068 v1 pith:T6U2S5EG submitted 2019-08-24 cs.NI cs.LO

Alex Horn , Ali Kheradmand , Mukul R. Prasad This is my paper · ORCID

classification cs.NIcs.LO

keywords networkverificationpacketequivalenceclassesatomicpredicatesmeet-semilatticeelementtypesmodelcountingemptyPECdetectionforwardingloop

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper claims that network verification can have full precision, broad expressiveness, and high speed in one method. Its #PEC algorithm replaces binary decision diagrams with a meet-semilattice of match conditions and decides whether a packet equivalence class is empty by counting the packet headers in it. Because empty equivalence classes are the source of non-minimal partitions, dropping them yields the unique minimal set of classes—the atomic predicates—without BDDs. The paper argues this makes precise analysis roughly 10 times faster than the BDD-based approach and makes new rule types, such as iptables-style ranges and complements, analyzable.

What carries the argument

The load-bearing object is a meet-semilattice of match conditions, represented as a Hasse diagram stored in a DAG. Each node stores an element, its direct child nodes, and a cardinality equal to the number of packet headers in the node's element minus the union of its children; a zero cardinality marks an empty packet equivalence class. Element types—such as IP prefixes, ranges, disjoint ranges, sets, tuples, and ternary bit vectors—are required only to form a finite partial order with a polynomial-time cardinality count. Insertion maintains the DAG incrementally while recording modified nodes, so cardinalities are recomputed only where the lattice changed. The counting step turns the coNP-hard emptiness question into arithmetic on machine words, which the paper identifies as the reason for the speed advantage.

What would settle it

Run #PEC on a small random set of match conditions, then independently brute-force the full closure under intersection, build the true Hasse diagram, and compare the non-empty packet equivalence classes and their cardinalities; any mismatch, or any difference when the same conditions are inserted in another order, refutes the optimality theorem. Replaying the paper's two-router example should also show the spurious forwarding loop disappear once empty classes are dropped.

Watch

Extended reading notes

Core claim

The central claim is the optimality theorem: for any set of match conditions expressible as element types, the non-empty packet equivalence classes constructed by #PEC are exactly the atomic predicates, the unique minimal partition of packet header space in which each match condition is a union of classes. The proof, in the appendix, shows that every non-empty class corresponds to a conjunction of input predicates and their negations, the same shapes atomic predicates have. The mechanism that makes this practical is cardinality-based emptiness detection: instead of solving a coNP-hard satisfiability search for a witness packet, #PEC computes the number of packet headers in each class by subtracting descendants' cardinalities from a node's element cardinality. The paper reports that this counting method is 10 to 100 times faster than SAT/SMT or BDD-based emptiness checks on real datasets.

Load-bearing premise

The load-bearing premise is that the incremental insertion procedure keeps the meet-semilattice's Hasse diagram exactly right after the added modified-node bookkeeping, because the paper cites an earlier proof of the unmodified procedure instead of proving the adaptation itself.

Editorial extensions

If this is right

Precise verification of forwarding loops, black holes, and reachability becomes applicable to rule sets that contain empty equivalence classes, where prior bit-vector tools produced both false alarms and missed shadowed rules.
Match conditions with arbitrary port ranges, sets of values, and field complements, such as those appearing in iptables rule-sets, can be handled without expanding them into bit vectors.
Atomic-predicate minimality can be achieved without binary decision diagrams, at roughly a ten-fold speed improvement over the BDD-based construction on the paper's datasets.
The partition constructed by #PEC is invariant under insertion order and under changes to rule priority or output action, so it can be reused as forwarding tables change.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Because the framework is defined abstractly over element types, other finite-set domains with polynomial counting—access-control lists, packet classification in switch hardware, or configuration differencing—could reuse the same construction for minimal partitions.
The practical speed of emptiness detection suggests that, for structured unions of sets, counting can outperform witness search even when the underlying decision problem is coNP-hard; testing this on other verification settings would show whether the lesson generalizes beyond packet headers.
A subtle robustness requirement: cardinality must be computed exactly, so implementations need overflow-safe arithmetic; any counter that wraps to zero on a genuinely non-empty class would reintroduce the very emptiness errors #PEC removes.
An implicit boundary is worst-case exponential lattice size, so the gains shown are empirical; pathological rule sets could still make the DAG too large for BDD-free construction.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The thing you should know about this paper is that the core idea is real: instead of building BDDs or TBVs, #PEC maintains a meet-semilattice over match conditions, and it detects empty PECs by exactly counting packet headers in each candidate class. The minimality theorem in Section III-F is not vacuous. The Appendix C proof, while a bit compressed, gives a credible argument that non-empty PECs coincide with Yang and Lam's atomic predicates. That is a genuine contribution: a lattice-based path to the same minimal partition, plus the cardinality emptiness check that ddNF lacks.

The stress-test note does not hold. Algorithm 2 line 16 is guarded by `if new`; the recursive call `INSERT_NODE(child, n')` only happens when the meet node is newly created. In the Figure 8 trace, the meet `e` already exists, so no recursion into `INSERT_NODE(c,e)` occurs. The self-loop and edge deletion in the stress-test scenario do not happen as described. That said, the adaptation from Kourie's algorithm does alter the recursion conditions, and the paper's correctness claim for Algorithm 2 is a one-line appeal to [35]. A rigorous re-proof, or even an invariant statement, is missing. That is a genuine soft spot, but not the fatal flaw the stress-test imagines.

Where the paper is weakest is the evaluation. The performance claims rest on re-implementations of APV and ddNF, with no released code, single-run measurements, no variance data, and APV's optional port aggregation deliberately disabled. That last choice is defensible — the authors argue it fairly — but it means the 10x claims are less convincing than they could be. The "longstanding quest" framing is also overheated; this is an incremental but solid algorithmic improvement within network verification, not a generational breakthrough.

Who should read this: people working on PEC construction, header space analysis, or real-time network invariants. They will get the core idea and can decide whether to trust the experiments. The paper deserves a serious referee, and I would send it out, but not for acceptance without code or reproducibility details and a more measured abstract.

Referee Report

4 major / 5 minor

Summary. The paper introduces #PEC, a lattice-theoretical framework for constructing packet equivalence classes (PECs) in network verification. The authors claim that #PEC combines the precision of atomic predicates (minimal PECs) with the expressiveness of arbitrary element types and the performance of ddNF, while avoiding BDDs. The technical core is an incremental meet-semilattice construction with per-node cardinalities, enabling detection of empty PECs by counting rather than by SAT/BDD search. The paper proves coNP-completeness of PEC emptiness, sketches a minimality proof for the generated non-empty PECs, presents case studies where ddNF gives wrong results because of empty PECs, and reports experiments showing speedups over APV and ddNF on real-world datasets.

Significance. If the central claims hold, the paper would make a valuable contribution by resolving a known tension among precision, expressiveness, and efficiency in PEC-based network verification. The proposed element-type abstraction is a clean generalization of TBVs, and the idea of using cardinalities to detect empty PECs is conceptually appealing and potentially useful beyond the specific network-verification setting. The minimality theorem, if fully supported, would put the construction on par with Yang and Lam's atomic predicates without BDDs. The case studies and the large experimental evaluation are also valuable. However, the manuscript's own text leaves the correctness of the central update algorithm under-proved, and the performance claims are not reproducible from the material provided. These issues are load-bearing for the paper's headline claims and require substantial revision.

major comments (4)

[Section III-D, Algorithm 2] The correctness of the DAG update is not established as printed. The pseudocode's block structure is ambiguous: line 16 (`INSERT_NODE(child, n')`) is indented under `if new`, but the surrounding `for`/`if` structure is not delimited, so it is unclear whether the recursion is guarded by `new` and whether lines 17--18 are inside the loop. If line 16 is executed even when `FIND_OR_CREATE_NODE` returns `new=false`, then the Figure 8 insertion sequence (inserting `f`, then `g=b∩f`, then meeting with the existing `e=c∩g`) reaches line 4 with equality on `c,e`, collects `e` in Γ, and lines 22--23 erase `e` from `c.children` and insert `e` into its own children, producing a self-loop and destroying the covering relation. If line 16 is guarded by `new` as the indentation suggests, the alleged self-loop does not arise, but the paper's statement that correctness "follows directly from the proof in [35]" is still not sufficient, because the edge updates at lines 17--23 and the `Modified Nodes` bookkeeping change the recursion and termination behavior of the original algorithm. This proof gap is load-bearing for the Theorem in Section III-F.
[Section III-D, Algorithm 3] Algorithm 3 has no invariant or proof that the deferred recomputation over `Modified Nodes` yields exact PEC cardinalities for all nodes after an arbitrary sequence of insertions. The algorithm subtracts descendant cardinalities from the input node's element cardinality and uses a local `visited` set, but there is no argument that (i) every modified descendant is recomputed before its parent's subtraction, (ii) the `Modified Nodes` erasure at line 14 cannot skip a node whose cardinality is still stale, and (iii) the order of processing in Algorithm 1 lines 6--7 is safe. Exact cardinalities are required for the emptiness detection and for the minimality theorem, so this is not merely a presentation issue.
[Section IV-A2, IV-D1] The performance claims (10--80x over APV and the comparisons with ddNF) are not reproducible from the manuscript. APV, ddNF, and #PEC are compared through a re-implementation of APV inside the authors' Z3-based framework; no source code or binary is released, no variance or repeated-run data are provided, and the optional port-aggregation preprocessing of APV is disabled. Since the abstract's speed claim is one of the paper's headline results, the comparison should be based on a released artifact or a third-party implementation, and should report run-to-run variation and the effect of port aggregation.
[Section IV-C] The claim that ddNF "misses 35 shadowed rules" and produces wrong answers in over 40 cases is not backed by a reproducible artifact or by detailed query and diagnostic listings; the section presents only illustrative examples. Because the empty-PEC phenomenon is the paper's central motivation for #PEC, please make the datasets, queries, and ddNF invocations available so that the counts and the reported false alarms and missed errors can be checked.

minor comments (5)

[Section III-E] The text contains a typo: "decribed" should be "described" in the discussion of query conversion.
[Section IV-D] The experimental setup says "Intel Xenon CPU ES-1660" but the CPU is almost certainly an Intel Xeon E5-1660; the typo should be corrected.
[Appendix D] Some table cells contain formatting artifacts, e.g., "0.0 66" for Stanford-Full/yozb, which should be 0.066; a full proofread of the tables is needed.
[Figure 11] The feature-comparison figure uses symbolic markers that need a legend or explicit textual labels; the meaning of the partially filled circles is not obvious, especially in a black-and-white copy.
[References] The reference to the Veriflow implementation as "personal communication" should be replaced with a publicly available implementation or a detailed description of the exact version used.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: #PEC's minimality claim is checked against Yang and Lam's external atomic-predicate definition, and cardinality is computed from element types rather than fitted.

full rationale

The paper's central theorem (Section III-F, with proof in Appendix C) compares #PEC's output against Yang and Lam's atomic predicates [27], an external benchmark with a separate uniqueness proof; the proof does not define atomic predicates in terms of #PEC. The DAG update algorithm is attributed to Kourie et al. [35], and the cardinality extension is a genuine addition, not a parameter fitted to the target result. The claim to detect empty PECs rests on the element-type cardinality operator and subtraction over the Hasse diagram, not on calibration against the datasets. The only same-author citation (Delta-net [14]) appears in related work and is not load-bearing for the minimality or correctness claims. The skeptical observation about Algorithm 2's unguarded recursive INSERT_NODE call identifies a possible correctness/termination bug, not circularity: a faulty adaptation of [35] would make the theorem unproved, but the theorem would not be true by definition because of the bug. No self-definitional, fitted-input, or self-citation-chain circularity is present.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central claim depends on the element type abstraction providing exact polynomial-time cardinality, and on the correctness of the external incremental lattice construction [35]. No new physical entities are introduced, and the algorithm itself has no fitted parameters.

free parameters (1)

BDD baseline tuning (initial node number, cache size) = manual tuning for better results in BuDDy
Chosen by hand in Section IV-A1 to make the BDD-based PEC-emptiness baseline perform as well as possible. This tuning affects the performance comparison but is not a parameter of #PEC itself.

assumptions (4)

domain assumption Element types form a finite partially ordered set with polynomial-time cardinality and are closed under intersection.
Section III-B states the two basic requirements for element types. The entire PEC construction and cardinality computation depend on these properties.
standard math The incremental lattice construction algorithm of Kourie et al. [35] correctly maintains the Hasse diagram of the meet-semilattice.
Section III-D says the correctness of the DAG edge updates follows directly from the proof in [35]. The paper does not re-prove this for its augmented algorithm.
standard math Atomic predicates as defined by Yang and Lam are unique and minimal.
Section III-F uses the definition of atomic predicates from [27] as the external benchmark for minimality.
domain assumption Query predicates are of the same element type as the match conditions and are present in the lattice after insertion.
Section III-E assumes each logical query is a Boolean combination of predicates with the same element type as the match conditions, ensuring FIND NODE never returns null in Algorithm 4.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification." pith.science (2026). https://pith.science/paper/T6U2S5EG

@misc{pith2026190809068,
  author       = {Pith},
  title        = {Pith review of: A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/T6U2S5EG}},
  note         = {Machine review of arXiv:1908.09068}
}

read the original abstract

Network verification promises to detect errors, such as black holes and forwarding loops, by logically analyzing the control or data plane. To do so efficiently, the state-of-the-art (e.g., Veriflow) partitions packet headers with identical forwarding behavior into the same packet equivalence class (PEC). Recently, Yang and Lam showed how to construct the minimal set of PECs, called atomic predicates. Their construction uses Binary Decision Diagrams (BDDs). However, BDDs have been shown to incur significant overhead per packet header bit, performing poorly when analyzing large-scale data centers. The overhead of atomic predicates prompted ddNF to devise a specialized data structure of Ternary Bit Vectors (TBV) instead. However, TBVs are strictly less expressive than BDDs. Moreover, unlike atomic predicates, ddNF's set of PECs is not minimal. We show that ddNF's non-minimality is due to empty PECs. In addition, empty PECs are shown to trigger wrong analysis results. This reveals an inherent tension between precision, expressiveness and performance in formal network verification. Our paper resolves this tension through a new lattice-theoretical PEC-construction algorithm, #PEC, that advances the field as follows: (i) #PEC can encode more kinds of forwarding rules (e.g., ip-tables) than ddNF and Veriflow, (ii) #PEC verifies a wider class of errors (e.g., shadowed rules) than ddNF, and (iii) on a broad range of real-world datasets, #PEC is 10X faster than atomic predicates. By achieving precision, expressiveness and performance, this paper answers a longstanding quest that has spanned three generations of formal network analysis techniques.

Figures

Figures reproduced from arXiv: 1908.09068 by the authors.

**Figure 2.** Verification: is there a forwarding loop, or not? [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗

**Figure 4.** Wrong result in ddNF, due to non-minimal PECs [PITH_FULL_IMAGE:figures/full_fig_p003_4.png] view at source ↗

Figures from the paper (10 more)

**Figure 6.** Figure 6: PECs due to the match conditions (colored rows) [PITH_FULL_IMAGE:figures/full_fig_p004_6.png]

**Figure 5.** Figure 5: Six semi-meetlattice elements induced by the three 3 [PITH_FULL_IMAGE:figures/full_fig_p004_5.png]

**Figure 8.** Figure 8: Two meet-semilattices (a and b) for different subset [PITH_FULL_IMAGE:figures/full_fig_p006_8.png]

**Figure 9.** Figure 9: Summary of datasets all children in Cx are mutually incomparable, i.e., for any child c and c ′ in Cx, neither c ⊂ c ′ nor c ′ ⊂ c. To implement the propositional logic PEC-emptiness solutions, we construct the following Boolean formula: x ∧ ¬W c∈Cx c —equivalently, …

**Figure 10.** Figure 10: Evaluation results for a subset of datasets. See App [PITH_FULL_IMAGE:figures/full_fig_p009_10.png]

**Figure 11.** Figure 11: Feature comparison of closest related work [PITH_FULL_IMAGE:figures/full_fig_p010_11.png]

**Figure 13.** Figure 13: Venn diagram of three match conditions, denoted [PITH_FULL_IMAGE:figures/full_fig_p013_13.png]

**Figure 14.** Figure 14: Internals of disjoint_ranges where the MAX constant corresponds to the maximal upper bound of any range APPENDIX B IMPLEMENTATION DETAILS In this appendix, we give more details regarding the implementation of element types. Since it is easy to implement ip_prefix, op…

**Figure 15.** Figure 15: Evaluation results for datasets that encode match c [PITH_FULL_IMAGE:figures/full_fig_p016_15.png]

**Figure 16.** Figure 16: Evaluation results for iptables rule-sets [PITH_FULL_IMAGE:figures/full_fig_p016_16.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

90 extracted references · 79 canonical work pages

[35]

An incremental algorithm to construct a lattice of set interse ctions,

D. G. Kourie, S. Obiedkov, B. W. Watson, and D. van der Mer we, “An incremental algorithm to construct a lattice of set interse ctions,” Sci. Comput. Program., vol. 74, no. 3, Jan. 2009

work page 2009
[1]

Making middleboxes someone else’s problem: Netw ork processing as a cloud service,

J. Sherry, S. Hasan, C. Scott, A. Krishnamurthy, S. Ratna samy, and V . Sekar, “Making middleboxes someone else’s problem: Netw ork processing as a cloud service,” in SIGCOMM, 2012

2012
[2]

CrystalNet: Faithfully emulating large production networks,

H. H. Liu, Y . Zhu, J. Padhye, J. Cao, S. Tallapragada, N. P . Lopes, A. Rybalchenko, G. Lu, and L. Y uan, “CrystalNet: Faithfully emulating large production networks,” in SOSP, 2017

2017
[3]

A quantitative study of ﬁrewall conﬁguration e rrors,

A. Wool, “A quantitative study of ﬁrewall conﬁguration e rrors,” Com- puter, vol. 37, no. 6, Jun. 2004

2004
[4]

Taxonomy of conﬂicts in networ k security policies,

H. Hamed and E. Al-Shaer, “Taxonomy of conﬂicts in networ k security policies,” IEEE Comm. Mag. , vol. 44, no. 3, Mar. 2006

2006
[5]

Trends in ﬁrewall conﬁguration errors: Measur ing the holes in swiss cheese,

A. Wool, “Trends in ﬁrewall conﬁguration errors: Measur ing the holes in swiss cheese,” IEEE Internet Computing , vol. 14, no. 4, Jul. 2010

2010
[6]

A general approach to network con- ﬁguration analysis,

A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Go vindan, R. Mahajan, and T. Millstein, “A general approach to network con- ﬁguration analysis,” in NSDI, 2015

2015
[7]

Fast control plane analysis using an abstract representation,

A. Gember-Jacobson, R. Viswanathan, A. Akella, and R. Ma hajan, “Fast control plane analysis using an abstract representation,” in SIGCOMM, 2016

2016

Show all 90 references

[8]

Efﬁcient network reachability a nalysis using a succinct control plane representation,

S. K. Fayaz, T. Sharma, A. Fogel, R. Mahajan, T. D. Millste in, V . Sekar, and G. V arghese, “Efﬁcient network reachability a nalysis using a succinct control plane representation,” in OSDI), 2016

2016
[9]

A genera l approach to network conﬁguration veriﬁcation,

R. Beckett, A. Gupta, R. Mahajan, and D. Walker, “A genera l approach to network conﬁguration veriﬁcation,” in SIGCOMM, 2017

2017
[10]

Debugging the data plane with Anteater,

H. Mai, A. Khurshid, R. Agarwal, M. Caesar, P . B. Godfrey , and S. T. King, “Debugging the data plane with Anteater,” in SIGCOMM, 2011

2011
[11]

Header space analysis: Static checking for networks,

P . Kazemian, G. V arghese, and N. McKeown, “Header space analysis: Static checking for networks,” in NSDI, 2012

2012
[12]

Real time network policy checking using header sp ace analysis,

P . Kazemian, M. Chang, H. Zeng, G. V arghese, N. McKeown, and S. Whyte, “Real time network policy checking using header sp ace analysis,” in NSDI, 2013

2013
[13]

V eriﬂow system analysis and optimization ,

C. Zhongbo, “V eriﬂow system analysis and optimization ,” Master’s thesis, University of Illinois Urbana-Champaign, 2014

2014
[14]

Delta-net: Real -time network veriﬁcation using atoms,

A. Horn, A. Kheradmand, and M. Prasad, “Delta-net: Real -time network veriﬁcation using atoms,” in NSDI, 2017

2017
[15]

Reachability analysis for AWS-based networks,

J. Backes, S. Bayless, B. Cook, C. Dodge, A. Gacek, A. J. H u, T. Kahsai, B. Kocik, E. Kotelnikov, J. Kukovec, S. McLaughlin, J. Reed, N. Rungta, J. Sizemore, M. A. Stalzer, P . Srinivasan, P . Subotic, C. V ar ming, and B. Whaley, “Reachability analysis for AWS-based networks...

2019
[16]

On static reachability analysis of IP networks,

G. G. Xie, J. Zhanm, D. A. Maltz, H. Zhang, A. Greenberg, G . Hjalm- tysson, and J. Rexford, “On static reachability analysis of IP networks,” in INFOCOM, 2005

2005
[17]

Model checking ﬁrewall policy conﬁgura- tions,

A. Jeffrey and T. Samak, “Model checking ﬁrewall policy conﬁgura- tions,” in POLICY, 2009

2009
[18]

The Margrave tool for ﬁrewall analysis,

T. Nelson, C. Barratt, D. J. Dougherty, K. Fisler, and S. Krishnamurthi, “The Margrave tool for ﬁrewall analysis,” in LISA, 2010

2010
[19]

FlowChecker: Conﬁguration analysis and veriﬁcation of federated OpenFlow infrastructures,

E. Al-Shaer and S. Al-Haj, “FlowChecker: Conﬁguration analysis and veriﬁcation of federated OpenFlow infrastructures,” in SafeConﬁg , 2010

2010
[20]

Model checking invariant security properties in OpenFlow,

S. Son, S. Shin, V . Y egneswaran, P . A. Porras, and G. Gu, “ Model checking invariant security properties in OpenFlow,” in ICC, 2013

2013
[21]

V eriﬁcat ion and synthesis of ﬁrewalls using sat and qbf,

S. Zhang, A. Mahmoud, S. Malik, and S. Narain, “V eriﬁcat ion and synthesis of ﬁrewalls using sat and qbf,” in ICNP, 2012

2012
[23]

V eriCon: Towards verifying controller programs in software-deﬁned networks,

T. Ball, N. Bjørner, A. Gember, S. Itzhaky, A. Karbyshev , M. Sagiv, M. Schapira, and A. V aladarsky, “V eriCon: Towards verifying controller programs in software-deﬁned networks,” in PLDI, 2014

2014
[24]

Detect ion and prevention of ﬁrewall-rule conﬂicts on software-deﬁned ne tworking,

F. A. Maldonado-Lopez, E. Calle, and Y . Donoso, “Detect ion and prevention of ﬁrewall-rule conﬂicts on software-deﬁned ne tworking,” in RNDM, 2015

2015
[25]

Checking beliefs in dynamic networks,

N. P . Lopes, N. Bjørner, P . Godefroid, K. Jayaraman, and G. V arghese, “Checking beliefs in dynamic networks,” in NSDI, 2015

2015
[26]

FLOWGUARD: Buildi ng robust ﬁrewalls for software-deﬁned networks,

H. Hu, W. Han, G.-J. Ahn, and Z. Zhao, “FLOWGUARD: Buildi ng robust ﬁrewalls for software-deﬁned networks,” in HotSDN, 2014

2014
[27]

Real-time veriﬁcation of network properties using atomic predicates,

H. Y ang and S. S. Lam, “Real-time veriﬁcation of network properties using atomic predicates,” in ICNP, 2013

2013
[28]

ddNF: An efﬁcient data structure for header spaces,

N. Bjørner, G. Juniwal, R. Mahajan, S. A. Seshia, and G. V arghese, “ddNF: An efﬁcient data structure for header spaces,” in HVC, 2016

2016
[29]

V eriﬁcation of switching network properti es using satisﬁ- ability,

R. McGeer, “V eriﬁcation of switching network properti es using satisﬁ- ability,” in ICC, 2012

2012
[30]

V eriFlow: V erifying network-wide invariants in real time,

A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P . B. Godfrey , “V eriFlow: V erifying network-wide invariants in real time,” in NSDI, 2013

2013
[31]

Graph-based algorithms for boolean func tion manipula- tion,

R. E. Bryant, “Graph-based algorithms for boolean func tion manipula- tion,” IEEE Trans. Comput. , vol. 35, no. 8, pp. 677–691, Aug. 1986

1986
[32]

D. E. Knuth, The Art of Computer Programming, V olume 4, Fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams , 12th ed. Addison-Wesley, 2009

2009
[33]

V eriﬁed iptables ﬁrewall analysis,

C. Diekmann, J. Michaelis, M. Haslbeck, and G. Carle, “V eriﬁed iptables ﬁrewall analysis,” in IFIP Networking , 2016

2016
[34]

B. A. Davey and H. A. Priestley, Introduction to Lattices and Order , 2nd ed. Cambridge University Press, 2002

2002
[36]

Instruction latencies, throughputs and micro - operation breakdowns for intel, amd and via cpus,

A. Fog, “Instruction latencies, throughputs and micro - operation breakdowns for intel, amd and via cpus,” https://www.agner.org/optimize/instruction tables.pdf
[37]

Ca cheﬂow: Dependency-aware rule-caching for software-deﬁned netwo rks,

N. Katta, O. Alipourfard, J. Rexford, and D. Walker, “Ca cheﬂow: Dependency-aware rule-caching for software-deﬁned netwo rks,” in SOSR, 2016

2016
[38]

Cardigan: Sdn distributed ro uting fabric going live at an internet exchange,

J. Stringer, D. Pemberton, Q. Fu, C. Lorier, R. Nelson, J . Bailey, C. N. Correa, and C. E. Rothenberg, “Cardigan: Sdn distributed ro uting fabric going live at an internet exchange,” in ISCC, 2014

2014
[39]

Route Views, http://www.routeviews.org/
[40]

Z3: An efﬁcient SMT solver,

L. De Moura and N. Bjørner, “Z3: An efﬁcient SMT solver,” in TACAS, 2008

2008
[41]

The SMT-LIB St andard: V ersion 2.6,

C. Barrett, P . Fontaine, and C. Tinelli, “The SMT-LIB St andard: V ersion 2.6,” Department of Computer Science, The University of Iow a, Tech. Rep., 2017, available at www.SMT-LIB.org

2017
[42]

Khurshid and B

A. Khurshid and B. Godfrey, personal communication, Ja n. 2019

2019
[43]

Lessons from building static analysis tools at google,

C. Sadowski, E. Aftandilian, A. Eagle, L. Miller-Cusho n, and C. Jaspan, “Lessons from building static analysis tools at google,” Commun. ACM, vol. 61, no. 4, pp. 58–66, Mar. 2018

2018
[44]

Pr edicting network futures with plankton,

S. Prabhu, A. Kheradmand, B. Godfrey, and M. Caesar, “Pr edicting network futures with plankton,” in APNet, 2017

2017
[45]

An analysis of BGP converge nce properties,

T. G. Grifﬁn and G. Wilfong, “An analysis of BGP converge nce properties,” in SIGCOMM, 1999

1999
[46]

Detecting BGP conﬁgu ration faults with static analysis,

N. Feamster and H. Balakrishnan, “Detecting BGP conﬁgu ration faults with static analysis,” in NSDI, 2005

2005
[47]

Modeling the routing of an auto nomous system with C-BGP,

B. Quoitin and S. Uhlig, “Modeling the routing of an auto nomous system with C-BGP,” IEEE Network , vol. 19, no. 6, Nov. 2005

2005
[48]

FSR: Formal analysis and implem entation toolkit for safe interdomain routing,

A. Wang, L. Jia, W. Zhou, Y . Ren, B. T. Loo, J. Rexford, V . N igam, A. Scedrov, and C. Talcott, “FSR: Formal analysis and implem entation toolkit for safe interdomain routing,” IEEE/ACM Transactions on Net- working, vol. 20, no. 6, Dec. 2012

2012
[49]

Formal semantics and automated veriﬁcation fo r the border gateway protocol,

K. Weitz, D. Woos, E. Torlak, M. D. Ernst, A. Krishnamurt hy, and Z. Tatlock, “Formal semantics and automated veriﬁcation fo r the border gateway protocol,” in NetPL, 2016

2016
[50]

Efﬁcient network reachability analysis usin g a succinct control plane representation,

S. K. Fayaz, T. Sharma, A. Fogel, R. Mahajan, T. Millstei n, V . Sekar, and G. V arghese, “Efﬁcient network reachability analysis usin g a succinct control plane representation,” in OSDI, 2016

2016
[51]

Plankton: Scalable network conﬁguration veriﬁcation thr ough model checking,

S. Prabhu, K. Y . Chou, A. Kheradmand, B. Godfrey, and M. C aesar, “Plankton: Scalable network conﬁguration veriﬁcation thr ough model checking,” in NSDI, 2020

2020
[52]

Detecting and re solving policy misconﬁgurations in access-control systems,

L. Bauer, S. Garriss, and M. K. Reiter, “Detecting and re solving policy misconﬁgurations in access-control systems,” ACM Transactions on Information and System Security , vol. 14, no. 1, Jun. 2011

2011
[53]

Automatic error ﬁnding in access-control policies,

K. Jayaraman, V . Ganesh, M. Tripunitara, M. Rinard, and S. Chapin, “Automatic error ﬁnding in access-control policies,” in CCS, 2011

2011
[54]

FIREMAN: A toolkit for ﬁrewall modeling and analysis,

L. Y uan, J. Mai, Z. Su, H. Chen, C.-N. Chuah, and P . Mohapa tra, “FIREMAN: A toolkit for ﬁrewall modeling and analysis,” in SP, 2006

2006
[55]

A NICE way to test openﬂow applications,

M. Canini, D. V enzano, P . Pereˇ s´ ıni, D. Kosti´ c, and J.Rexford, “A NICE way to test openﬂow applications,” in NSDI, 2012

2012
[56]

Correct by construction netwo rks using stepwise reﬁnement

L. Ryzhyk, N. Bjørner, M. Canini, J.-B. Jeannin, C. Schl esinger, D. B. Terry, and G. V arghese, “Correct by construction netwo rks using stepwise reﬁnement.” in NSDI, 2017

2017
[57]

Auto matic test packet generation,

H. Zeng, P . Kazemian, G. V arghese, and N. McKeown, “Auto matic test packet generation,” in CoNEXT, 2012

2012
[58]

Towards test-driven software deﬁned networking,

D. Lebrun, S. Vissicchio, and O. Bonaventure, “Towards test-driven software deﬁned networking,” in NOMS, 2014

2014
[59]

Cha os monkey: Increasing sdn reliability through systematic network des truction,

M. A. Chang, B. Tschaen, T. Benson, and L. V anbever, “Cha os monkey: Increasing sdn reliability through systematic network des truction,” in SIGCOMM, 2015

2015
[60]

BU ZZ: Testing context-dependent policies in stateful networks,

S. K. Fayaz, T. Y u, Y . Tobioka, S. Chaki, and V . Sekar, “BU ZZ: Testing context-dependent policies in stateful networks,” in NSDI, 2016

2016
[61]

An assertion language for debugging SDN applications,

R. Beckett, X. K. Zou, S. Zhang, S. Malik, J. Rexford, and D. Walker, “An assertion language for debugging SDN applications,” in HotSDN, 2014

2014
[62]

Troubleshooting blackbox SDN control softwar e with minimal causal sequences,

C. Scott, A. Wundsam, B. Raghavan, A. Panda, A. Or, J. Lai , E. Huang, Z. Liu, A. El-Hassany, S. Whitlock, H. Acharya, K. Zariﬁs, an d S. Shenker, “Troubleshooting blackbox SDN control softwar e with minimal causal sequences,” in SIGCOMM, 2014

2014
[63]

Stati c differential program analysis for software-deﬁned networks,

T. Nelson, A. D. Ferguson, and S. Krishnamurthi, “Stati c differential program analysis for software-deﬁned networks,” in FM, 2015

2015
[64]

SDNRacer: Detecting concurrency violations in software- deﬁned net- works,

J. Miserez, P . Bielik, A. El-Hassany, L. V anbever, and M . V echev, “SDNRacer: Detecting concurrency violations in software- deﬁned net- works,” in SOSR, 2015

2015
[65]

BigB ug: Practical concurrency analysis for SDN,

R. May, A. El-Hassany, L. V anbever, and M. V echev, “BigB ug: Practical concurrency analysis for SDN,” in SOSR, 2017

2017
[66]

Optimizing Horn solvers for network repair,

H. Hojjat, P . R¨ ummer, J. McClurg, P . ˇCern` y, and N. Foster, “Optimizing Horn solvers for network repair,” in FMCAD, 2016

2016
[67]

Automat- ically repairing network control planes using an abstract r epresentation,

A. Gember-Jacobson, A. Akella, R. Mahajan, and H. H. Liu , “Automat- ically repairing network control planes using an abstract r epresentation,” in SOSP, 2017

2017
[68]

Auto mated bug removal for software-deﬁned networks

Y . Wu, A. Chen, A. Haeberlen, W. Zhou, and B. T. Loo, “Auto mated bug removal for software-deﬁned networks.” in NSDI, 2017

2017
[69]

Don’t mind the gap: Bridging network-wide objectives and d evice-level conﬁgurations,

R. Beckett, R. Mahajan, T. Millstein, J. Padhye, and D. W alker, “Don’t mind the gap: Bridging network-wide objectives and d evice-level conﬁgurations,” in SIGCOMM, 2016

2016
[70]

Network-wide conﬁguration synthesis,

A. El-Hassany, P . Tsankov, L. V anbever, and M. V echev, “Network-wide conﬁguration synthesis,” in CA V, 2017

2017
[71]

Net2Text: Query-Guided Summarization of Network Forwarding Behavio rs,

R. Birkner, D. Drachlser-Cohen, L. V anbever, and M. V echev, “Net2Text: Query-Guided Summarization of Network Forwarding Behavio rs,” in NSDI, 2018

2018
[72]

Frenetic: A network programming la nguage,

N. Foster, R. Harrison, M. J. Freedman, C. Monsanto, J. R exford, A. Story, and D. Walker, “Frenetic: A network programming la nguage,” in ICFP, 2011

2011
[73]

Concurre nt NetCore: From policies to pipelines,

C. Schlesinger, M. Greenberg, and D. Walker, “Concurre nt NetCore: From policies to pipelines,” in ICFP, 2014

2014
[74]

NetKA T: Semantic foundatio ns for networks,

C. J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Koz en, C. Schlesinger, and D. Walker, “NetKA T: Semantic foundatio ns for networks,” in POPL, 2014

2014
[75]

Kinetic: V eriﬁable dynamic network control

H. Kim, J. Reich, A. Gupta, M. Shahbaz, N. Feamster, and R . J. Clark, “Kinetic: V eriﬁable dynamic network control.” in NSDI, 2015

2015
[76]

P4K: a formal semantics of P4 and applications,

A. Kheradmand and G. Rosu, “P4K: a formal semantics of P4 and applications,” CoRR, vol. abs/1804.01468, 2018

2018 arXiv
[77]

Abstractions for network update,

M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, an d D. Walker, “Abstractions for network update,” in SIGCOMM, 2012

2012
[78]

HotSwap: Correct and efﬁcient controller upgrades for software-deﬁ ned networks,

L. V anbever, J. Reich, T. Benson, N. Foster, and J. Rexfo rd, “HotSwap: Correct and efﬁcient controller upgrades for software-deﬁ ned networks,” in HotSDN, 2013

2013
[79]

Safe update of hybrid SDN networks,

S. Vissicchio, L. V anbever, L. Cittadini, G. G. Xie, and O. Bonaventure, “Safe update of hybrid SDN networks,” IEEE/ACM Transactions on Networking, vol. 25, no. 3, Jun. 2017

2017
[80]

Decentralized c onsistent updates in SDN,

T. D. Nguyen, M. Chiesa, and M. Canini, “Decentralized c onsistent updates in SDN,” in SOSR, 2017

2017
[81]

Libra: Divide and conquer to verify forwardi ng tables in huge networks,

H. Zeng, S. Zhang, F. Y e, V . Jeyakumar, M. Ju, J. Liu, N. Mc Keown, and A. V ahdat, “Libra: Divide and conquer to verify forwardi ng tables in huge networks,” in NSDI, 2014

2014
[82]

Network conﬁguration in a box: towards end-to-end veriﬁcation of ne twork reachability and security,

E. Al-Shaer, W. Marrero, A. El-Atawy, and K. El-Badawi, “Network conﬁguration in a box: towards end-to-end veriﬁcation of ne twork reachability and security,” in ICNP, 2009

2009
[83]

A utomated analysis and debugging of network connectivity policies,

K. Jayaraman, N. Bjørner, G. Outhred, and C. Kaufman, “A utomated analysis and debugging of network connectivity policies,” Microsoft Research, Tech. Rep., 2014

2014
[84]

Scaling network veriﬁcation using symmetry and surge ry,

G. D. Plotkin, N. Bjørner, N. P . Lopes, A. Rybalchenko, a nd G. V argh- ese, “Scaling network veriﬁcation using symmetry and surge ry,” in POPL, 2016

2016
[85]

Contro l plane compression,

R. Beckett, A. Gupta, R. Mahajan, and D. Walker, “Contro l plane compression,” in SIGCOMM, 2018

2018
[86]

Use of BGP for r outing in large-scale data centers,

P . Lapukhov, A. Premji, and J. Mitchell, “Use of BGP for r outing in large-scale data centers,” RFC 7938, Aug. 2016

2016
[87]

APPENDIX A WORST -CASE COMPLEXITY Here we prove results about the theoretical worst-case complexity of #PEC’s underlying model counting method

ISO, International Standard ISO/IEC 14882:2017(E) Programming Lan- guage C++ , 2017. APPENDIX A WORST -CASE COMPLEXITY Here we prove results about the theoretical worst-case complexity of #PEC’s underlying model counting method. Given a pair ⟨x, Y ⟩ where x is an element (reca...

2017
[88]

on input of a DNF formula φ over n Boolean variables, convert each clause ck in φ to a n-length ternary bit vector vk, as deﬁned in § A
[89]

collect these n-length ternary bit vectors into set V
[90]

send V to oracle to obtain the cardinality of PEC⟨⊤, V ⟩
[91]

subtract PEC⟨⊤, V ⟩’s cardinality from 2n. Example. We continue § A. Suppose the three clauses in the DNF formula φ represent match conditions. The number of packet headers in the disjunction of these match conditions is then 23 − 4 = 4 , since ⊤ : 4 according to Figure 12 whe...

1958

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [35]

An incremental algorithm to construct a lattice of set interse ctions,

D. G. Kourie, S. Obiedkov, B. W. Watson, and D. van der Mer we, “An incremental algorithm to construct a lattice of set interse ctions,” Sci. Comput. Program., vol. 74, no. 3, Jan. 2009

work page 2009

[2] [1]

Making middleboxes someone else’s problem: Netw ork processing as a cloud service,

J. Sherry, S. Hasan, C. Scott, A. Krishnamurthy, S. Ratna samy, and V . Sekar, “Making middleboxes someone else’s problem: Netw ork processing as a cloud service,” in SIGCOMM, 2012

2012

[3] [2]

CrystalNet: Faithfully emulating large production networks,

H. H. Liu, Y . Zhu, J. Padhye, J. Cao, S. Tallapragada, N. P . Lopes, A. Rybalchenko, G. Lu, and L. Y uan, “CrystalNet: Faithfully emulating large production networks,” in SOSP, 2017

2017

[4] [3]

A quantitative study of ﬁrewall conﬁguration e rrors,

A. Wool, “A quantitative study of ﬁrewall conﬁguration e rrors,” Com- puter, vol. 37, no. 6, Jun. 2004

2004

[5] [4]

Taxonomy of conﬂicts in networ k security policies,

H. Hamed and E. Al-Shaer, “Taxonomy of conﬂicts in networ k security policies,” IEEE Comm. Mag. , vol. 44, no. 3, Mar. 2006

2006

[6] [5]

Trends in ﬁrewall conﬁguration errors: Measur ing the holes in swiss cheese,

A. Wool, “Trends in ﬁrewall conﬁguration errors: Measur ing the holes in swiss cheese,” IEEE Internet Computing , vol. 14, no. 4, Jul. 2010

2010

[7] [6]

A general approach to network con- ﬁguration analysis,

A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Go vindan, R. Mahajan, and T. Millstein, “A general approach to network con- ﬁguration analysis,” in NSDI, 2015

2015

[8] [7]

Fast control plane analysis using an abstract representation,

A. Gember-Jacobson, R. Viswanathan, A. Akella, and R. Ma hajan, “Fast control plane analysis using an abstract representation,” in SIGCOMM, 2016

2016