Verification of distributed protocols using decidable logics

Speaker:
Oded Padon - CS-Lecture
Date:
Monday, 13.1.2020, 10:30
Place:
Room 601 Taub Bld.
Affiliation:
Stanford University

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 already handles challenging examples that other state-of-the-art techniques cannot handle. I will briefly describe several other works, including a new optimization technique for deep learning computations that achieves significant speedups relative to existing deep learning frameworks. Short Bio: ========== Oded Padon is a postdoc at Stanford University, hosted by Alex Aiken, working on programming languages and formal methods research. He completed his PhD from Tel Aviv University, advised by Mooly Sagiv.

Back to the index of events