Computational Verification of Network Programs in Coq
We report on the design of the first fully automatic, machine-checked
tool suite for verification of high-level network programs. The tool
suite targets programs written in NetCore, a new declarative network
programming language. Our work builds on a recent effort by Guha,
Reitblatt, and Foster to build a machine-verified compiler from
NetCore to OpenFlow, a new protocol for software-defined networking.