Interactive verification of distributed protocols
Distributed protocols such as Paxos play an important role in many computer systems.
Therefore, a bug in a distributed protocol may have tremendous effects.
Accordingly, a lot of effort has been invested in verifying such protocols.
However, due to the infinite state space (e.g., unbounded number of nodes, messages) and protocols complexity, verification is both undecidable and hard in practice.
I will describe a deductive approach for verification of distributed protocols, based on first-order logic, inductive invariants and user interaction.
The use of first-order logic and a decidable fragment of universally quantified invariants allows to completely automate some verification tasks.
Tasks that remain undecidable (e.g. finding inductive invariants) are solved with user interaction, based on graphically displayed counterexamples.
I will also describe the application of these techniques to verify safety of several variants of Paxos, and a way to extend the approach to verify liveness and temporal properties.
Oded Padon is a fourth year PhD student in Tel Aviv University, under the supervision of Prof. Mooly Sagiv. His research focuses on verification of distributed protocols using first-order logic.
He is a recipient of the 2017 Google PhD fellowship in programming languages.