Reseña: “Computational verification of network programs in Coq”

Se ha publicado un artículo de verificación formal en Coq titulado Computational verification of network programs in Coq.

Su autor es Gordon Stewart (miembro del proyecto Verified Software Toolchain la Universidad de Princeton).

Su resumen es

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. The result is an end-to-end system that provides strong guarantees on the compiled OpenFlow flow tables that are installed on actual network switches.

El correspondiente código en Coq se encuentra aquí.