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
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.