• Blog >
  • Goldilocks the Verification Engineer

Categories

Goldilocks the Verification Engineer

  • Date Wednesday, March 27, 2019  Time 11:00 AM
  • Speaker James Wilcox, PhD student at the University of Washington
  • Location Galois Inc., 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

    The presentation will be live streamed on Galois's YouTube channel.

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.