Declarative Network Verification

Abstract. In this paper, we present our initial design and implementation of a declarative network verifier (DNV). DNV utilizes theorem proving, a well established verification technique where logic-based axioms that automatically capture network semantics are generated, and a userdriven proof process is used to establish network correctness properties. DNV takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical axioms that can be directly used in existing theorem provers to validate protocol correctness. DNV is a significant improvement compared to existing use case of theorem proving which typically require several man-months to construct the system specifications. Moreover, NDlog, a high-level specification, whose semantics are precisely compiled into DNV without loss, can be directly executed as implementations, hence bridging specifications, verification, and implementation. To validate th...

• Type: Conference
• Year: 2009
• Where: PADL
• Authors: Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky
• Keywords: DNV Utilizes Theorem, Network Correctness Properties, PADL 2009, Programming Languages, PVS Theorem Prover