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. All individuals must show the Daily Screener green pass in order to gain entry to the building.


How to Subscribe