| ||||
| ||||
![]() Title:Deductive Verification of Distributed Protocols in First-Order Logic Authors:Oded Padon Conference:FMCAD 2018 Tags:Decidable logics, Deductive verification, Distributed systems, Effectively propositional logic, Liveness verification, Paxos and Safety verification Abstract: In this tutorial, we will explore a practical approach to using first order-logic, and a decidable fragment thereof, to prove complex distributed protocols and systems. The approach, implemented in the Ivy verification tool, applies abstraction and modular reasoning techniques to mitigate the expressiveness limitations of decidable fragments. The high-level strategy involves the following ideas:
Experience to date indicates that the approach, based on first-order logic, is surprisingly powerful, and it is possible to prove safety and liveness properties of complex protocols (e.g., Paxos variants), and also to produce verified low-level implementations, using decidable logics. Moreover, the effort required to structure the proof in this way is more than repaid by greater reliability of proof automation, which significantly reduces the overall verification effort. Better matching human reasoning capabilities to the capabilities of automated provers results in a more stable and predictable formal development process. This tutorial is based on joint works with Jochen Hoenicke, Neil Immerman, Aleksandr Karbyshev, Giuliano Losa, Kenneth L. McMillan, Aurojit Panda, Andreas Podelski, Mooly Sagiv, Sharon Shoham, Marcelo Taube, James R. Wilcox, and Doug Woos Deductive Verification of Distributed Protocols in First-Order Logic ![]() Deductive Verification of Distributed Protocols in First-Order Logic | ||||
Copyright © 2002 – 2025 EasyChair |