Skip to content (access key 's')
Logo of Technion
Logo of CS Department


Verification of distributed protocols using decidable logics
event speaker icon
Oded Padon - CS-Lecture
event date icon
Monday, 13.1.2020, 10:30
event location icon
Room 601 Taub Bld.
Advisor:  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]