Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

Also keep in mind that you will need to write a paper summary for your choice of papers throughout the semester.


Read the paper Machine-Verified Network Controllers by Guha et al.

Why are we reading this paper?

What to learn from this paper?

Answer this question

Suppose you are building a network using NetCore, with several servers dedicated to monitoring traffic (in the same sense as the paper's example of logging HTTP traffic). Different traffic (e.g., based on destination address or destination port) gets logged to different servers. How would you formally prove that, on the real network as implemented by OpenFlow switches, all traffic is getting logged to some server? What theorem statements would you need to state in Coq, and what parts of NetCore's formal framework would help you in your proof?