Goldilocks the Verification Engineer

Abstract:

In this talk, I will describe three approaches to verifying distributed systems using inductive invariants: manual proof, automated proof, and invariant inference. These techniques offer increasing levels of automation, but at some cost. I will argue that the middle technique strikes a good balance for users, and that it is possible for a tool to be so automated as to be unusable. The talk will include an extended demo/walkthrough using a just-right automated verification tool to verify a simple distributed system.

Bio:

James Wilcox is a 6th-and-final-year PhD student at the University of Washington in the Paul G. Allen School of Computer Science & Engineering, where he is advised by Zach Tatlock. James’s research interests include programming languages, formal verification, distributed systems, and 3d printing. Outside of research, James enjoys singing in far too many choirs and dreaming of his next bike, canoe, or bike/canoe tour.