Synthesizing Formal Network Specifications From Input-Output Examples

We propose, a tool that synthesizes network specifications in a declarative logic programming language from input-output examples. aims to accelerate the adoption of formal verification in networking practice, by reducing the effort and expertise required to specify network models or properties. aims to be i) highly expressive, capable of synthesizing network specifications with complex semantics; ii) scalable, by virtue of using a novel best-first search algorithm to efficiently explore an unbounded solution space, and iii) robust, avoiding the need for exhaustive input-output examples by actively generating new examples. Our experiments demonstrate that can synthesize a wide range of specifications used in network verification, analysis, and implementations. Furthermore, improves upon existing approaches in terms of expressiveness, robustness to examples, and the quality of synthesized programs.