Synthesizing Formal Network Specifications from Input-Output Examples
IEEE/ACM Transactions on Networking(2023)
摘要
We propose NetSpec, a tool that synthesizes network specifications in a declarative logic programming language from input-output examples. NetSpec aims to accelerate the adoption of formal verification in networking practice, by reducing the effort and expertise required to specify network models or properties. NetSpec 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 NetSpec can synthesize a wide range of specifications used in network verification, analysis, and implementations. Furthermore, NetSpec improves upon existing approaches in terms of expressiveness, robustness to examples, and the quality of synthesized programs.
更多查看译文
关键词
Routing protocols,Benchmark testing,Consensus protocol,Task analysis,Semantics,Security,Runtime,Network protocol,program synthesis
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要