IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2019 > Deductive verification of distributed protocols in first-order logic
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Mooly Sagiv

miércoles 12 de junio de 2019

10:45am Meeting room 302 (Mountain View), level 3

Mooly Sagiv, Research Professor, Tel Aviv University, Israel

Deductive verification of distributed protocols in first-order logic


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 decidable fragments of first-order logic, inductive invariants and user interaction. The use of decidable fragments of first-order logic 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.

This work is part of a Ph.D. by Oded Padon The ideas were integrated into Ivy It is joint work with Giuliano Losa, Jochen Hoenicke, Ken McMillan, Aurojit Panda, Sharon Shoham, Marcelo Taube, James R. Wilcox, and Doug Woos.