Formal Foundations for Networks

Опубликовано 8 августа 2016, 18:16

In many fields of computing, techniques ranging from testing to formal modeling to full-blown verification have been successfully used to build reliable systems. But networks have largely resisted analysis using formal techniques. This talk will present recent work on developing a mathematical foundation for networks including a detailed operational model of software-defined networks, its formalization in the Coq proof assistant, a machine-verified compiler and run-time system for the NetCore programming language, and an automatic property-checking tool based on Z3. Joint work with Arjun Guha, Mark Reitlbatt, and Rebecca Coombes. A forthcoming paper in the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) describes our system in further detail.