Verification of distributed protocols using decidable logics
Speaker: Oded Padon, Stanford University
Location: 60 Fifth Avenue 150
Date: February 21, 2020, 11 a.m.
Host: Michael Overton
Formal verification of infinite-state systems, and distributed systems in particular, is a long-standing research goal. I will describe a series of works that develop a methodology for verifying distributed algorithms and systems using decidable logics, employing decomposition, abstraction, and user interaction. This methodology is implemented in an open-source tool, and has resulted in the first mechanized proofs of several important distributed protocols. I will also describe a novel approach to the problem of invariant inference based on a newly formalized duality between reachability and mathematical induction. The duality leads to a primal-dual search algorithm, and a prototype implementation is already able to automatically find invariants for challenging distributed protocols that other state-of-the-art techniques cannot handle.
Oded Padon is a postdoc at Stanford University, advised by Alex Aiken, working on programming languages and formal methods research. He completed his PhD from Tel Aviv University, advised by Mooly Sagiv.
Refreshments will be offered starting 15 minutes prior to the scheduled start of the talk.