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:

Refreshments will be offered starting 15 minutes prior to the scheduled start of the talk.


How to Subscribe