A (Co)algebraic Approach to Programming and Verifying Computer Networks

Other Titles
As computer networks have grown into some of the most complex and critical computing systems today, the means of configuring them have not kept up: they remain manual, low-level, and ad-hoc. This makes network operations expensive and network outages due to misconfigurations commonplace. The thesis of this dissertation is that high-level programming languages and formal methods can make network configuration dramatically easier and more reliable. The dissertation consists of three parts. In the first part, we develop algorithms for compiling a network programming language with high-level abstractions to low-level network configurations, and introduce a symbolic data structure that makes compilation efficient in practice. In the second part, we develop foundations for a probabilistic network programming language using measure and domain theory, showing that continuity can be exploited to approximate (statistics of) packet distributions algorithmically. Based on this foundation and the theory of Markov chains, we then design a network verification tool that can reason about fault-tolerance and other probabilistic properties, scaling to data-center-size networks. In the third part, we introduce a general-purpose (co)algebraic framework for designing and reasoning about programming languages, and show that it permits an almost linear-time decision procedure for program equivalence. We hope that the framework will serve as a foundation for efficient verification tools, for networks and beyond, in the future.
Journal / Series
Volume & Issue
316 pages
Date Issued
coalgebra; compilers; domain-specific programming languages; Kleene Algebra; software defined networking; verification
Effective Date
Expiration Date
Union Local
Number of Workers
Committee Chair
Foster, Nate
Committee Co-Chair
Committee Member
Kozen, Dexter Campbell
Kleinberg, Robert David
Degree Discipline
Computer Science
Degree Name
Ph. D., Computer Science
Degree Level
Doctor of Philosophy
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
Link(s) to Reference(s)
Previously Published As
Government Document
Other Identifiers
Attribution-NoDerivatives 4.0 International
dissertation or thesis
Accessibility Feature
Accessibility Hazard
Accessibility Summary
Link(s) to Catalog Record