How do you model network behaviour in a way that is amenable to mostly-automated formal reasoning?
At Curry On Conference, Associate Professor, Nate Foster showed us how we can make computer networks and formals methods work for us!
Formal Methods and Computer Networks - A Match Made in Heaven?
Computer networks provide the essential communication fabric that underpins almost all modern computing systems. Yet today, most networks are built and operated in an ad hoc manner and require frequent interventions from human experts to remain functional.
This talk will make the case for bringing ideas from the formal methods community to bear on practical problems in networking. Starting with the network forwarding plane, we will show how to model network behavior in a way that is amenable to mostly-automated formal reasoning. We will then show how these lower-level models can be used to guide efforts to verify higher layers of the stack, such as the network control planes and even application-level functions.
This talk was given by Nate Foster at Curry On Conference.