A Theorem Proving Approach towards Declarative Networking

We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative networking, a recent innovation that enables network protocols to be concisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, network designer can supply a component-based model of their routing design, automatically generate PVS specifications for verification and subsequent compilation into veriffied declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying