EECS Special Seminar: Oded Padon "Verification of distributed protocols using decidable logics"

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.

Bio:
Oded Padon is a a postdoctoral scholar at Stanford University, advised by Alex Aiken. His research interests are programming languages and formal methods. He completed his PhD from Tel Aviv University, advised by Mooly Sagiv.