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.
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.