Pith. sign in

REVIEW 3 major objections 5 minor 42 references

StacKAT: Infinite State Network Verification

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read StacKAT adds a stack to NetKAT and still makes program equivalence decidable

desk verdict StacKAT is a genuine theoretical advance for network verification, but the decision procedure as stated has a correctness gap (bisimilarity vs language equivalence) that needs fixing before the main decidability theorem is trustworthy. read the letter →

arxiv 2506.13383 v1 pith:HHZPBZHW submitted 2025-06-16 cs.PL

Jules Jacobs , Nate Foster , Tobias Kappé , Dexter Kozen , Lily Saada , Alexandra Silva , Jana Wagemaker This is my paper · ORCID
classification cs.PL MSC 68Q4568Q6068M12
keywords StacKATNetnetworkverificationprogramequivalencedecisionprocedurestackautomataKleenealgebrapushdownlanguages
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

StacKAT extends the network verification language NetKAT with push and pop operations on a packet stack, so programs can model parsing, source routing, telemetry, tunneling, and MPLS. The paper's central claim is that equivalence of such programs remains decidable even though the stack gives them infinitely many states. The proof works by reading each program as a regular expression over push and pop actions, then canonicalizing its trace language: cancel matching push-pop pairs, discard mismatched ones, and add pop-push pairs that are semantically invisible. Two programs are equivalent exactly when their canonicalized trace languages agree, and the canonical languages are regular enough to compare by finite automata. A complete axiomatization is given for the push-pop fragment.

What carries the argument

The load-bearing object is the canonicalized trace language $\bar L(e)$, produced in three steps: (1) pushpop closure adds shortcuts for matching $\mathrm{push}(v)\cdot\mathrm{pop}(v)$; (2) filtering intersects with $\mathrm{pop}^*\mathrm{push}^*$, keeping only traces where all pops precede all pushes; (3) poppush closure inserts $\mathrm{pop}(v)\cdot\mathrm{push}(v)$ pairs, implemented on automata by zipping the trace from the middle outward, representing a word $\mathrm{pop}(1)\mathrm{pop}(2)\mathrm{push}(3)\mathrm{push}(4)$ as $(\mathrm{pop}(2),\mathrm{push}(3))(\mathrm{pop}(1),\mathrm{push}(4))$, and prepending $((\mathrm{pop}(v),\mathrm{push}(v)))^*$. The zipped automaton makes the otherwise non-regular poppush closure regular, so language equivalence of the resulting automata is decidable and yields counterexamples.

What would settle it

Search small value domains for two push-pop programs whose canonical trace automata accept the same language but whose input-output relations differ on some stack, e.g., by exhaustive enumeration of programs up to modest size; the paper's Theorem 3.7 predicts none exists. A more targeted check verifies Lemma 3.10 directly by computing $[\bar L]$ and $[\bar L]'$ for a collection of canonical languages and comparing them.

Watch

Extended reading notes

Core claim

The paper establishes Theorem 3.7: for push-pop StacKAT programs $e,f$, semantic equivalence $\llbracket e\rrbracket=\llbracket f\rrbracket$ holds iff $\bar L(e)=\bar L(f)$, where $\bar L=\mathrm{poppush}(\mathrm{filter}(\mathrm{pushpop}(L)))$. It extends this to full StacKAT via trace languages $\mathrm{traces}^{\alpha_2}_{\alpha_1}(e)$ for each input/output packet-header pair $(\alpha_1,\alpha_2)$, giving Theorem 4.2 and a decision procedure in EXPSPACE (Theorem 4.5), with PSPACE-completeness for the push-pop fragment (Theorems 3.13 and 3.14). For push-pop programs the paper also gives a complete equational axiomatization (Theorem 6.9): Kleene algebra plus $\mathrm{push}(v)\mathrm{pop}(v)=1$, $\mathrm{push}(v)\mathrm{pop}(w)=0$ for $v\neq w$, the inequality $\mathrm{pop}(v)\mathrm{push}(v)\le 1$, and a rule that transfers provability through a new operator $\dagger$.

Load-bearing premise

The argument assumes that inserting pop-then-push pairs in the middle of canonical traces captures exactly the behavior of stacks with extra values underneath, so that no semantic difference is lost in the canonicalized language.

Editorial extensions

If this is right

  • Every StacKAT equivalence query, such as reachability, waypointing, correct compilation, and slice isolation, can be answered mechanically instead of by hand.
  • Inequivalent programs come with an explicit input-output packet pair witnessing the difference, computed from the symmetric difference of the canonical automata.
  • The push-pop fragment has a sound and complete axiomatization, so equivalence proofs can be carried out equationally as well as algorithmically.
  • Full StacKAT equivalence is EXPSPACE-complete, matching the hardness of regular expressions with squaring; with a fixed set of header variables the bound drops to PSPACE.

Reading between the lines

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

  • The zipping construction may generalize: any action language whose valid traces form $\mathrm{pop}^*\mathrm{push}^*$ can be decided by reading from the middle outward, which could apply to other stack-like models beyond network packets.
  • The paper's contrast with visibly pushdown languages suggests a broader lesson: removing the input tape while keeping an unrestricted stack is what buys decidability, so similar tape-less stack models elsewhere may also have decidable equivalence.
  • A symbolic implementation, e.g., BDD-style as the paper leaves to future work, would be the natural test of whether the EXPSPACE procedure scales to realistic header spaces; the paper's own benchmarks show header enumeration is the bottleneck.
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.

Referee Report

3 major / 5 minor

Summary. The paper introduces StacKAT, an extension of NetKAT with push and pop stack operations over a finite value set, and studies the equivalence problem for StacKAT programs. The main claims are: (i) equivalence in the pure push-pop fragment is decidable by canonicalizing the trace language through push-pop cancellation, filtering to pop* push* traces, and pop-push closure, then comparing the resulting zipped trace languages (Theorems 3.7 and 3.12); (ii) equivalence for full StacKAT, including header tests and assignments, reduces to equivalence of header-parameterized trace languages (Theorem 4.2), giving an EXPSPACE decision procedure (Theorem 4.5); (iii) counterexamples can be extracted when programs are inequivalent; and (iv) a complete axiomatization for the push-pop fragment is provided using a new dagger operator on languages (Theorem 6.9). The paper includes a detailed appendix with proofs, an interactive implementation, and benchmarks.

Significance. If the results are correct, this is a substantial contribution: StacKAT is a natural infinite-state extension of NetKAT, and the paper shows that its equivalence problem remains decidable despite the presence of a stack, with a matching EXPSPACE algorithm and a completeness result for the push-pop fragment. The central technical idea, zipping trace languages so that the non-regular pop-push closure becomes a regular precomposition A* · zip(L), is elegant and useful. The paper also ships a working implementation and benchmarks, which strengthens confidence that the constructions are concretely realizable. The main caveats are that Theorem 3.12 states a bisimilarity check that is not justified for the nondeterministic automata built by the construction, and that the load-bearing Lemma 3.10 is only proved by a two-sentence sketch. Both issues appear repairable within the paper's scope.

major comments (3)
  1. [Section 3.4, Theorem 3.12] The stated decision procedure says to 'check bisimilarity of these resulting automata,' but the constructed automata are NFAs in general. Figure 6 creates initial states (q,q), epsilon transitions, and simultaneous backward-pop/forward-push steps without determinization, and the precomposition with A* in Lemma 3.6 adds further nondeterminism. For NFAs, bisimilarity is strictly stronger than language equivalence, so a bisimilarity check can reject semantically equivalent programs and is not justified by Theorem 3.7, which is stated in terms of language equality. The complexity argument in Section 3.5 and the implementation description in Section 5.1 rely on language equivalence, not bisimilarity. Please replace the bisimilarity check with an explicit language-equivalence check on the canonicalized automata (or prove that the constructed automata are deterministic or complete in a sense that makes bisimilarity coincide with language equivalence), and update the counterexample-extraction wording in Section 5 accordingly.
  2. [Section 3.4, Lemma 3.10] Lemma 3.10 is load-bearing for Theorem 3.7: it identifies [Lbar] with [Lbar]' and is the only step that lets Lemma 3.11 be applied. The proof, however, is only a two-sentence sketch: the inclusion ⊆ is justified by saying that poppush(L) adds strings with pop(v)push(v) pairs that 'precisely match the possible additional values in the stack.' This is not a routine detail: the converse inclusion requires showing, for every residual context of stack values below the explicit stack content, that an inserted pop-push word makes the exact-stack semantics reach the same output. Please provide a full proof, for example by induction on the length of the residual stack, making explicit how the closure rules in Figure 4 supply the required words.
  3. [Section 4, Theorem 4.2 and Lemma 4.3] The decidability of full StacKAT is a headline result, but the proof of Lemma 4.3 is only summarized as proving two inclusions by induction, and Theorem 4.2 is described as 'entirely analogous' to Theorem 3.7. The header-annotated trace semantics introduces a genuine interaction: tests and assignments are compiled into automaton states, so the adaptation of Lemmas 3.9 and 3.10 to the annotated setting must be shown explicitly. Please give the full inductive proof of Lemma 4.3 and spell out how the canonicalization lemmas transfer to the pairs (α1, α2), rather than leaving the transfer to analogy.
minor comments (5)
  1. [Section 4.1] The finiteness argument for the trace automaton says the automaton steps only to expressions of the form e1·e2···ek where 'each ei is strictly smaller than ei+1,' but the ordering is not defined; please state the measure on expressions explicitly.
  2. [Section 3.2] The claim that (push(3)^n)*·(pop(3)^m)* is equivalent to (push(3)^gcd(n,m))* + (pop(3)^gcd(n,m))* is stated without proof; if kept, add a reference or a short derivation.
  3. [Section 5.1] The benchmark descriptions do not report the size of the value domain V, the number of header fields, or the hardware used; please include these details for reproducibility.
  4. [Section 7] There is a duplicated phrase in 'Below, we review below the most closely related work'; please fix the typo.
  5. [Throughout] The bar/overline notation for Lbar and a-bar is easy to lose in print, especially when it distinguishes push and pop letters; consider using a more robust notation such as subscripted or bracketed symbols.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: StacKAT's equivalence decision procedure is proved against an independently defined relational semantics, not assumed into existence.

full rationale

The paper's central claim is that semantic equivalence JeK=JfK coincides with equality of canonical trace languages Lbar(e)=Lbar(f). This is not circular. The semantics J−K is defined directly in Figure 1 as a relation on packets, independently of Lbar. The trace language L(e) is the ordinary regular language of push/pop words of the expression, and Lbar is obtained by three syntactic operations (pushpop closure, filtering to pop*push*, poppush closure) whose definitions do not mention J−K or the equivalence relation being decided. The soundness of each canonicalization with respect to the semantics is proved: Lemma 3.8 (JeK=[L(e)]), Lemma 3.9 ([L]=[Lbar]), Lemma 3.10 ([Lbar]=[Lbar]'), and Lemma 3.11 (exact-stack languages equal iff languages equal). Theorem 3.7 is then proved by chaining these lemmas. Even though the poppush operation is motivated by the semantic axiom pop(v)push(v)+1=1, the operation is defined on languages, and the fact that it exactly accounts for residual stack content is an argued lemma (Lemma 3.10), not an assumption. The full-language extension (Theorem 4.2) is likewise reduced to the push-pop case via trace languages traces_alpha2_alpha1(e), whose faithful representation of semantics is proved in Lemma 4.3. There are no fitted parameters and no predictions that are defined as their own outputs. The axiomatization in Section 6 is also non-circular: it proves normal-form transformations using Brzozowski derivatives and Kleene algebra, then reduces completeness to Kozen's external completeness theorem for KA; the new rule (5) is justified by the bijection K of Lemma 6.7, not by assuming the equivalence it is meant to prove. Self-citations, including NetKAT foundations, KATch, and Silva's thesis for the fundamental theorem, are background or standard external results and are not load-bearing: the decidability argument does not require accepting any self-cited paper's contested claim. Separately, without treating it as circularity, Theorem 3.12's phrase 'check bisimilarity' is in tension with the language-equivalence check used in Section 3.5 and Section 5.1; this is a correctness concern, not a reduction of the result to its own inputs. Overall, the derivation chain is self-contained modulo standard automata and Kleene algebra facts.

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

No free parameters are fitted. The central machinery relies on finite header and value domains, standard automata theory, and Kleene algebra completeness. The only new formal object, the dagger operator, is a proof device for the completeness theorem and is not an empirical posit.

assumptions (4)
  • domain assumption Values V and header fields F are finite, and packet headers are records over F to V (Figure 1).
    This finiteness makes the trace automaton finite for full StacKAT and the header-pair enumeration in Section 4 possible; it is part of the language definition, not an empirical claim.
  • domain assumption The stack is unbounded and there is no separate input tape; a packet is a pair of header and stack.
    This single-stack, no-tape model is what keeps equivalence decidable; the paper argues that adding an input tape makes it undecidable (Section 3, Section 7).
  • standard math Kleene algebra completeness theorem (Kozen 1994) and Brzozowski derivative finiteness are used as black boxes.
    Used in Theorems 6.2 and 6.3 to prove normal form transformation and completeness, and in the dagger completeness proof for the regular language R.
  • standard math Standard results on pushdown automata and regular expression equivalence complexity (e.g., PSPACE-completeness) are relied on.
    Used for Theorems 3.13, 3.14, 4.4, and 4.5, and for claims about VPLs, Dyck languages, and one-counter automata in Section 7.
invented entities (2)
  • StacKAT language
    purpose: Models network programs with finite header fields plus an unbounded stack; expresses parsing, source routing, telemetry, and tunneling.
    A formal language design, not an empirical posit; its usefulness is assessed through the theorems and examples.
  • dagger operator (†) on languages
    purpose: Forms languages {xx | x in B} to capture the non-regular part of pop-push canonicalization in the completeness proof.
    A syntactic proof device in Section 6.2; it has no falsifiable empirical handle, which is expected for a mathematical construction.

how reviews work

0 comments
Cite this review

Pith. "Pith review of StacKAT: Infinite State Network Verification." pith.science (2026). https://pith.science/paper/HHZPBZHW

@misc{pith2026250613383,
  author       = {Pith},
  title        = {Pith review of: StacKAT: Infinite State Network Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HHZPBZHW}},
  note         = {Machine review of arXiv:2506.13383}
}
read the original abstract

We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and - most importantly - access to a stack with accompanying push and pop operations. By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like NetKAT. We develop a decision procedure for StacKAT program equivalence, based on finite automata. This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs. Finally, we provide an axiomatization of StacKAT equivalence and establish its completeness.

Figures

Figures reproduced from arXiv: 2506.13383 by the authors.

Figure 1
Figure 1. StacKAT syntax, meaning, and semantics. Contributions. Overall, this paper makes the following contributions. • The design of StacKAT, a domain specific language for infinite state network verification that can model a wide range of network behaviors, such as packet parsing, source routing, telemetry, tunneling, MPLS, and more (Section 2) • A decision procedure that verifies the semantic equivalence of two StacKAT p… view at source ↗
Figure 2
Figure 2. Push-pop canonicalization of a language 𝐿 We then show that language equivalence of the canonicalized languages implies semantic equivalence of the original StacKAT programs: J𝑒K = J𝑓 K ⇐⇒ 𝐿(𝑒) = 𝐿(𝑓 ) We proceed to describe the canonicalization steps in detail, and then show how to extend the decision procedure to StacKAT programs with local variables. 3.1 Push-Pop Canonicalization Let us assume that we have a Stac… view at source ↗
Figure 3
Figure 3. Push-pop closure rules. Given the presence of the solid edges, we add the dotted edge. For each [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: Pop-push canonicalization of a language 𝐿 general, we cannot remove traces without considering the full context—i.e., possible interactions between different traces. We conjecture that the resulting operation would be exceedingly difficult to define and compute, partic…
Figure 5
Figure 5. Figure 5: Zipping the trace language; in these equations„ [PITH_FULL_IMAGE:figures/full_fig_p011_5.png]
Figure 6
Figure 6. Figure 6: Zipping the trace automaton Zipping the Trace Automaton. In order to make use of zip for the decision procedure, we need to define a zipping operation on the automaton level. Given an automaton for a language 𝐿, the zipped automaton for zip(𝐿) should traverse the origi…
Figure 7
Figure 7. Figure 7: The trace language of a StacKAT program. [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]
Figure 8
Figure 8. Figure 8: The transitions of the trace automaton of a StacKAT program. [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Performance comparison of all benchmarks. The x-axis shows the number of operations or depth for [PITH_FULL_IMAGE:figures/full_fig_p017_9.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 16 canonical work pages

  1. [1]

    Madhusudan

    Rajeev Alur and P. Madhusudan. 2004. Visibly pushdown languages. InSTOC. doi:10.1145/1007352.1007390

    arXiv 2004

  2. [2]

    Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. InPOPL. doi:10.1145/2535838.2535862

    arXiv 2014

  3. [3]

    Antimirov

    Valentin M. Antimirov. 1996. Partial Derivatives of Regular Expressions and Finite Automaton Constructions.Theor. Comput. Sci.(1996). doi:10.1016/0304-3975(95)00182-4

    doi:10.1016/0304-3975(95)00182-4 1996

  4. [4]

    Ryan Beckett and Aarti Gupta. 2022. Katra: Realtime Verification for Multilayer Networks. InNSDI. https://www. usenix.org/conference/nsdi22/presentation/beckett

    work page 2022

  5. [5]

    Jean Berstel and Luc Boasson. 2002. Balanced Grammars and Their Languages. InFormal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg. doi:10.1007/3-540-45711-9_1

    doi:10.1007/3-540-45711-9_1 2002

  6. [6]

    Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. 2014. P4: Programming Protocol-Independent Packet Processors. SIGCOMM(07 2014). doi:10.1145/2656877.2656890

    arXiv 2014

  7. [7]

    Ahmed Bouajjani, Javier Esparza, and Oded Maler. 1997. Reachability Analysis of Pushdown Automata: Application to Model-Checking. InCONCUR. doi:10.1007/3-540-63141-0_10

    doi:10.1007/3-540-63141-0_10 1997

  8. [8]

    Brzozowski

    Janusz A. Brzozowski. 1964. Derivatives of Regular Expressions.J. ACM(1964). doi:10.1145/321239.321249

    arXiv 1964

Show all 42 references
  1. [9]

    Buckheister and Georg Zetzsche

    P. Buckheister and Georg Zetzsche. 2013. Semilinearity and Context-Freeness of Languages Accepted by Valence Automata. InMFCS. doi:10.1007/978-3-642-40313-2_22

    2013 doi

  2. [10]

    Amina Doumane, Denis Kuperberg, Damien Pous, and Cécilia Pradic. 2019. Kleene Algebra with Hypotheses. In FOSSACS. doi:10.1007/978-3-030-17127-8_12

    2019 doi

  3. [11]

    Alain Finkel, Bernard Willems, and Pierre Wolper. 1997. A direct symbolic approach to model checking pushdown systems. InWorkshop on Verification of Infinite State Systems. doi:10.1016/S1571-0661(05)80426-8

    1997 doi

  4. [12]

    Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. InPOPL. doi:10.1145/2676726.2677011

    2015

  5. [13]

    Hopcroft, Rajeev Motwani, and Jeffrey D

    John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006.Introduction to Automata Theory, Languages, and Computation (3rd Edition)

    2006

  6. [14]

    Reps, and Shmuel Sagiv

    Susan Horwitz, Thomas W. Reps, and Shmuel Sagiv. 1995. Demand Interprocedural Dataflow Analysis. InSIGSOFT. doi:10.1145/222124.222146

    1995

  7. [15]

    Jesper Stenbjerg Jensen, Troels Beck Krøgh, Jonas Sand Madsen, Stefan Schmid, Jirí Srba, and Marc Tom Thorgersen

  8. [16]

    Peter Gjøl Jensen, Dan Kristiansen, Stefan Schmid, Morten Konggaard Schou, Bernhard Clemens Schrenk, and Jirí Srba

  9. [17]

    Peter Gjøl Jensen, Stefan Schmid, Morten Konggaard Schou, Jirí Srba, Juan Vanerio, and Ingo van Duijn. 2021. Faster Pushdown Reachability Analysis with Applications in Network Verification. InATV A. doi:10.1007/978-3-030-88885- 5_12

    2021 doi

  10. [18]

    Adam Husted Kjelstrøm and Andreas Pavlogiannis. 2022. The decidability and complexity of interleaved bidirected Dyck reachability. InPOPL. doi:10.1145/3498673

    2022 doi

  11. [19]

    Dexter Kozen. 1994. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events.Inf. Comput. (1994). doi:10.1006/inco.1994.1037

    1994

  12. [20]

    Dexter Kozen. 1996. Kleene algebra with tests and commutativity conditions. InTACAS. doi:10.1007/3-540-61042-1_35

    1996 doi

  13. [21]

    Vincent Mathieu and Jules Desharnais. 2005. Verification of Pushdown Systems Using Omega Algebra with Domain. InRelMICS/AKA. doi:10.1007/11734673_15

    2005 doi

  14. [22]

    Robert McNaughton. 1967. Parenthesis Grammars.J. ACM(1967). doi:10.1145/321406.321411 Proc. ACM Program. Lang., Vol. 9, No. PLDI, Article 158. Publication date: June 2025. 158:24 Jules Jacobs, Nate Foster, Tobias Kappé, Dexter Kozen, Lily Saada, Alexandra Silva, and Jana Wagemaker

    1967

  15. [23]

    Meyer and Larry J

    Albert R. Meyer and Larry J. Stockmeyer. 1972. The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space. InSW AT. doi:10.1109/SWAT.1972.29

    1972 doi

  16. [24]

    Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva. 2024. KATch: A Fast Symbolic Verifier for NetKAT. InPLDI. doi:10.1145/3656454

    2024 doi

  17. [25]

    Damien Pous, Jurriaan Rot, and Jana Wagemaker. 2024. On Tools for Completeness of Kleene Algebra with Hypotheses. LMCS(2024). doi:10.46298/LMCS-20(2:8)2024

    2024 doi

  18. [26]

    Jakob Rehof and Manuel Fähndrich. 2001. Type-base flow analysis: from polymorphic subtyping to CFL-reachability. InPOPL. doi:10.1145/360204.360208

    2001

  19. [27]

    Thomas W. Reps. 1998. Program analysis via graph reachability.Inf. Softw. Technol.40, 11-12 (1998), 701–726. doi:10.1016/S0950-5849(98)00093-7

    1998 doi

  20. [28]

    Reps, Susan Horwitz, and Shmuel Sagiv

    Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability. InPOPL. doi:10.1145/199448.199462

    1995

  21. [29]

    Reps, Susan Horwitz, Shmuel Sagiv, and Genevieve Rosay

    Thomas W. Reps, Susan Horwitz, Shmuel Sagiv, and Genevieve Rosay. 1994. Speeding up Slicing. InSIGSOFT. doi:10.1145/193173.195287

    1994

  22. [30]

    Reps, Stefan Schwoon, and Somesh Jha

    Thomas W. Reps, Stefan Schwoon, and Somesh Jha. 2003. Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis. InSAS. doi:10.1007/3-540-44898-5_11

    2003 doi

  23. [31]

    Reps, Stefan Schwoon, Somesh Jha, and David Melski

    Thomas W. Reps, Stefan Schwoon, Somesh Jha, and David Melski. 2005. Weighted pushdown systems and their application to interprocedural dataflow analysis.Sci. Comput. Program.(2005). doi:10.1016/J.SCICO.2005.02.009

    2005 doi

  24. [32]

    Reps, and Susan Horwitz

    Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz. 1996. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation.Theor. Comput. Sci.1&2 (1996). doi:10.1016/0304-3975(96)00072-2

    1996 doi

  25. [33]

    Géraud Sénizergues. 1997. The Equivalence Problem for Deterministic Pushdown Automata is Decidable. InICALP. doi:10.1007/3-540-63165-8_221

    1997 doi

  26. [34]

    Géraud Sénizergues. 2002. L(A) = L(B)? Decidability Results from Complete Formal Systems. InICALP. doi:10.1007/3- 540-45465-9_4

    2002 doi

  27. [35]

    Géraud Sénizergues. 2002. L(A)=L(B)? A simplified decidability proof.Theor. Comput. Sci.(2002). doi:10.1016/S0304- 3975(02)00027-0

    2002 doi

  28. [36]

    2010.Kleene Coalgebra

    Alexandra Silva. 2010.Kleene Coalgebra. Ph. D. Dissertation. Radboud Universiteit Nijmegen

    2010

  29. [37]

    Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha. 2015. A Fast Compiler for NetKAT. InICFP. doi:10.1145/2784731.2784761

    2015

  30. [38]

    Sunshine

    Carl A. Sunshine. 1977. Source routing in computer networks.Comput. Commun. Rev.(1977). doi:10.1145/1024853. 1024855

    1977 doi

  31. [39]

    Valiant and Michael S

    Leslie G. Valiant and Michael S. Paterson. 1975. Deterministic one-counter automata.J. Comput. Syst. Sci.(1975). doi:10.1016/S0022-0000(75)80005-5

    1975 doi

  32. [40]

    Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. InNSDI. https://www.usenix.org/conference/nsdi20/presentation/zhang-peng A Proofs Lemma 3.1.For any NFA over the alphabet Σ={push(𝑣),pop(𝑣)|𝑣∈𝑉} repre...

    2020

  33. [2018]

    InCoNEXT

    P-Rex: fast verification of MPLS networks with multiple link failures. InCoNEXT. doi:10.1145/3281411.3281432

  34. [2020]

    InCoNEXT

    AalWiNes: a fast and quantitative what-if analysis tool for MPLS networks. InCoNEXT. doi:10.1145/3386367. 3431308

    doi

Pith tools

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