Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn about QuASI, a novel system that addresses queue dynamics uncertainty in network management through a layered formal methods approach in this 16-minute conference presentation from NSDI '25. Discover how researchers from Princeton University developed a solution to answer queue-related queries using only coarse-grained per-port packet counts, overcoming the challenge that while queue lengths correlate with packet counts, deriving precise correlations is difficult due to missing information like packet arrival order. Explore the system's innovative two-layer architecture that employs a novel enqueue-rate abstraction and efficient algorithms to generate cover-sets of abstract traces, construct representative traces, and verify them using matrix existence results and SMT solvers. Understand how QuASI guarantees no false positives or negatives while achieving up to 106X faster performance than state-of-the-art solutions, enabling practical formal performance analysis for network debugging, monitoring, and analysis tasks using minute-granularity packet counts.
