一句话：提出带栈的网络验证语言 StacKAT，并给出基于有限自动机的等价判定与完备公理化。
现有 NetKAT 等网络验证语言难以建模解析、源路由和遥测等需要栈结构的行为。论文提出 StacKAT，将有限状态变量与栈分别视为已解析报文头和待解析内容，支持循环、有限状态变量、非确定性与 push/pop 操作，从而表达无限状态网络程序。作者基于有限自动机为 StacKAT 程序等价性设计判定过程，可验证全网性质并在程序不等价时给出反例；同时给出等价公理化并证明其完备性。
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.
@article{paperbot3111,
title = {StacKAT: Infinite State Network Verification},
author = {Jules Jacobs and Nate Foster and Tobias Kappé and Dexter Kozen and Lily Saada and Alexandra Silva and Jana Wagemaker},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729257}
}