More Like this

1. Kirigami, the Verifiable Art of Network Cutting

   https://doi.org/10.1109/TNET.2024.3360371  

   Thijm, Timothy Alberdingk; Beckett, Ryan; Gupta, Aarti; Walker, David (June 2024, IEEE/ACM Transactions on Networking)

   Satisfiability Modulo Theories (SMT)-based analysis allows exhaustive reasoning over complex distributed control plane routing behaviors, enabling verification of converged routing states under arbitrary conditions. To improve scalability of SMT solving, we introduce a modular verification approach to network control plane verification, where we cut a network into smaller fragments. Users specify an annotated cut which describes how to generate these fragments from the monolithic network, and we verify each fragment independently, using these annotations to define assumptions and guarantees over fragments akin to assume-guarantee reasoning. We prove that any converged states of the fragments are converged states of the monolithic network, and there exists an annotated cut that can generate fragments corresponding to any converged state of the monolithic network. We implement this procedure as Kirigami, an extension of the network verification language and tool NV, and evaluate it on industrial topologies with synthesized policies. We observe a 10x improvement in end-to-end NV verification time, with SMT solve time improving by up to 6 orders of magnitude. 

   more » « less
2. Sound Termination and Non-termination Analysis of C Programs with Bit-Precise Bounded Semantics and Advanced Constructs

   https://doi.org/10.1145/3808205  

   Fathi, Negar; Unno, Hiroshi; Terauchi, Tachio; Purandare, Rahul (June 2026, Proceedings of the ACM on Software Engineering)

   Program termination and non-termination analysis is a foundational problem in formal verification with important implications for software safety and reliability. Despite extensive research, existing techniques struggle with real-world C programs that manipulate complex data types such as pointers, arrays, and structures, or that perform low-level operations such as bitwise arithmetic and bounded integer computations. This paper introduces Athena, a framework for sound termination and non-termination analysis of C programs that models finite-width and bit-precise integer semantics and supports advanced constructs. Athena combines pointer-to-array rewriting, bounded integer semantics enforced via modulo arithmetic or bit-vector semantics, and an extended translation to Labeled Transition Systems (LTS), yielding structured, analyzable representations suitable for logic-based reasoning. Our analysis engine builds on MuVal, a modular verification engine based on the first-order fixpoint logic µCLP with background theories, and extends it with support for array, tuple, and bit-vector theories in ranking function synthesis and recurrent set detection. We evaluate Athena on the 2024 Termination Competition (TermCOMP) and on 117 real-world benchmarks featuring 445 non-termination bugs, after excluding benchmarks that rely on undefined behavior. It achieves 60.95% correctness on the real-world benchmarks and 76.28% on TermCOMP, while producing zero wrong results across both suites. These results highlight Athena’s strong combination of precision and soundness for the termination and non-termination analysis of complex C programs. 

   more » « less
3. Scalable verification of probabilistic networks

   https://doi.org/10.1145/3314221.3314639  

   Smolka, Steffen; Kumar, Praveen; Kahn, David M.; Foster, Nate; Hsu, Justin; Kozen, Dexter; Silva, Alexandra (June 2019, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation)

   This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT's scalability using real-world topologies, compare its performance against state-of-the-art tools, and develop an extended case study on a recently proposed data center network design. 

   more » « less
4. High-Fidelity Cellular Network Control-Plane Traffic Generation without Domain Knowledge

   https://doi.org/10.1145/3646547.3688422  

   Kong, Z Jonny; Hu, Nathan; Hu, Y Charlie; Meng, Jiayi; Koral, Yaron (November 2024, ACM)

   With rapid evolution of mobile core network (MCN) architectures, large-scale control-plane traffic (CPT) traces are critical to studying MCN design and performance optimization by the R&D community. The prior-art control-plane traffic generator SMM heavily relies on domain knowledge which requires re-design as the domain evolves. In this work, we study the feasibility of developing a high-fidelity MCN control plane traffic generator by leveraging generative ML models. We identify key challenges in synthesizing high-fidelity CPT including generic (to data-plane) requirements such as multimodality feature relationships and unique requirements such as stateful semantics and long-term (time-of-day) data variations. We show state-of-the-art, generative adversarial network (GAN)-based approaches shown to work well for data-plane traffic cannot meet these fidelity requirements of CPT, and develop a transformer-based model, CPT-GPT, that accurately captures complex dependencies among the samples in each traffic stream (control events by the same UE) without the need for GAN. Our evaluation of CPT-GPT on a large-scale control-plane traffic trace shows that (1) it does not rely on domain knowledge yet synthesizes control-plane traffic with comparable fidelity as SMM; (2) compared to the prior-art GAN-based approach, it reduces the fraction of streams that violate stateful semantics by two orders of magnitude, the max y-distance of sojourn time distributions of streams by 16.0%, and the transfer learning time in deriving new hourly models by 3.36×. 

   more » « less
5. Inference-Time Conformal Reasoning with Valid Factuality Control for Large Language Models

   Wang, Ting; Shi, Yuanjie; Yan, Yan; Zhang, Huan (July 2026, Proceedings of Machine Learning Research)

   Large language models (LLMs) increasingly perform multi-step reasoning, where intermediate claims form implicit directed acyclic graphs whose node correctness is structurally conditioned on their ancestors. This makes factuality uncertainty structural, rather than a trivial accumulation of node-wise errors, and necessitates inferencetime uncertainty quantification over the reasoning structure. While conformal prediction (CP) offers flexible user-specified factuality control, existing work remains post-hoc and cannot intervene during generation. To fill the gap between CP’s flexibility and its post-hoc limitation, we propose an Inference-Time Conformal Reasoning (ITCR) framework that integrates CP directly into reasoning graph generation. ITCR learns a structurelevel factuality uncertainty function that aggregates claim-level factuality signals over reasoning graphs without complex modeling assumptions. We then design the non-conformity score based on graph-level factuality uncertainty and calibrate the conformal threshold to decide when to stop generation. We theoretically show such generation is nested, yielding valid coverage guarantees for factuality control. Experiments over multiple datasets and coverage objectives demonstrate empirically valid coverage. In downstream reasoning tasks, inference-time calibrated graphs yield more accurate generation than post-hoc pruned graphs. 

   more » « less