This course provides an introduction to the emerging class of programming languages that are used to specify and verify behavior of computer networks. It will examine recent proposals based on logic, functional, and distributed languages, as well as tools for establishing correctness using tools such as automatic solvers, model checkers, and proof assistants.


  • HW 6 is released!
  • HW 5 is released!
  • HW 4 is released!
  • HW 3 is released!
  • HW 2 is released!
  • HW 1 is released!
  • The first lecture will be held on Thursday, August 29th.