6 papers
Network Analysis with Parametric NetKAT
Han Xu, Zachary Kincaid, David Walker
Network engineers often need to perform network diagnosis and inference tasks, which frequently require answers to enumeration questions such as "Which packets from the Internet ar…
Kleene Algebra with Transitive Commutativity Conditions
Han Xu, Chenyu Zhou, Zachary Kincaid +1
Kleene algebra (KA) provides a foundational algebraic framework for reasoning about program structure and control flow. To capture equivalences arising from reordering or independe…
A Categorical Basis for Robust Program Analysis
Zachary Kincaid, Shaowei Zhu
Users of program analyses expect that results change predictably in response to changes in their programs, but many analyses fail to provide such robustness. This paper introduces…
Software Model Checking via Summary-Guided Search (Extended Version)
Ruijie Fang, Zachary Kincaid, Thomas Reps
In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by…
Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
Shaowei Zhu, Zachary Kincaid
This paper studies the problem of synthesizing (lexicographic) polynomial ranking functions for loops that can be described in polynomial arithmetic over integers and reals. While…
Relational Network Verification
Xieyang Xu, Yifei Yuan, Zachary Kincaid +4
Relational network verification is a new approach to validating network changes. In contrast to traditional network verification, which analyzes specifications for a single network…