Colloquium Details
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
Synopsis:
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.
Speaker Bio:
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.
Notes:
In-person attendance only available to those with active NYU ID cards.