network, verification, synthesis, welcome,

Welcome to netverify.fun

Ratul Mahajan Ratul Mahajan View Apr 20, 2020 · 2 mins read
Ryan Beckett Ryan Beckett View Apr 20, 2020 · 2 mins read
Welcome to netverify.fun

Network verification and synthesis has emerged as an exciting research area at the intersection of networking, programming languages, and formal methods. Work in this area is motivated by the rapidly growing scale and complexity of modern networks and by the high frequency of network outages and security breaches. It aims to formally prove the correctness of (some aspects of) the network, raise the level of abstraction for network design, or develop methods that are correct by construction. Researchers have invented a range of approaches that cleverly combine ideas from hardware and software verification with domain-specific insights rooted in how networks function.

The real-world impact of this line of research is undeniable despite the fact that the research is relatively new. All large cloud providers are now using some form of network verification to ensure high availability for their networks. And several startups have emerged to translate promising research to mature technologies that can be used by a broad array of network engineers.

One side-effect of the newness of the area, and the speed at which it is evolving, is that it can be difficult to make sense of it, especially for researchers and practitioners who are not actively working in the area. It can be difficult to understand newly-developed techniques and difficult to tell how they fit into the overall picture (or, even, what is the overall picture?!). It is similarly difficult to tell which challenges have been effectively addressed and whichs ones remain open. These difficulties in turn make it harder for new researchers to enter into the area and for practitioners to judge which techniques are “shovel ready” for adoption in real networks.

Our goal with netverify.fun is to make network verification and synthesis research accessible to a broad audience. We intend for it to be a living site that explains the latest research, contains expert commentary that synthesizes what may appear to be disjointed developments, and provides opinions on important open problems.

The site of course cannot succeed without community engagement. If you work in this area, we invite you to write articles that explain your work to (non-networking) computer scientists and network engineers or, more generally, provide your perspective on the field. If you are a network engineer, we invite you to share your challenges and views on how existing research falls short. If you are a researcher that does not work in this area, we invite you to express your frustrations with research in the area or tell us what you’d like to see covered. Our intent is for the site to be diverse and inclusive of all viewpoints.

Contributing to the site is easy. Send pull requests to its GitHub repository with new articles or additions/corrections to existing ones; open issues for topics you would like to see covered; and participate in discussions about published articles. You are also welcome to drop us a line if you need a sounding board for your contribution ideas.

We are launching netverify.fun site with a piece that captures our view on network verification research, and we have a great line up of articles in the pipeline.

So, stay tuned!

Ratul Mahajan
Author Ratul Mahajan Follow
Ratul Mahajan is an Associate Professor at the University of Washington (Paul G. Allen School of Computer Science) and a Co-founder and CEO of Intentionet, a company that is enabling safe, rapid evolution of computer networks using formal analysis and high-level design approaches. Prior to that, he was a Principal Researcher at Microsoft Research. He got his PhD at the University of Washington and B.Tech at Indian Institute of Technology, Delhi, both in Computer Science and Engineering.
Ryan Beckett
Author Ryan Beckett
Ryan Beckett is a Computer Scientist in the Mobility and Networking research group at Microsoft. He holds a PhD from Princeton in Computer Science as well as a B.S. in Computer Science and a B.A. in Mathematics from the University of Virginia.