Buffy: A Formal Language-Based Framework for Network Performance Analysis

Despite recent advances in using formal methods for analyzing network performance, modeling network functionality for performance analysis remains challenging. Existing tools expect users to directly create the logical formulas corresponding to the network functionality of interest. This is often unintuitive, difficult to get right, and tightly coupled with the specific encoding and reasoning engine one chooses to use. Instead, we propose language abstractions that enable users to model network functionality and analysis tasks in an imperative solver-agnostic program, and a framework to transform them into a representation that can be analyzed by the appropriate solver. We outline our progress so far, demonstrating the potential of our approach through preliminary case studies and directions for future work.