Credits
The following people have contributed ideas, code or examples to IVy.
- Ken McMillan
University of Texas at Austin.
His projects page briefly describes Duality and Interpolating Z3 which are in the version of Z3 used here. - Oded Padon, Weizmann Institute of Science
- Aurojit Panda, NYU
- Mooly Sagiv, Tel Aviv University
- Sharon Shoham, Tel Aviv University
Ivy focused publications
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham
ACM SIGPLAN Notices, Volume 51, Issue 6
Pages 614 - 630
Published: 02 June 2016
https://dl.acm.org/doi/10.1145/2980983.2908118
McMillan, Kenneth
2016 Formal Methods in Computer-Aided Design (FMCAD), Mountain View, CA, USA, 2016
pp. 109-116, doi: 10.1109/FMCAD.2016.7886668.
https://doi.org/10.1109/FMCAD.2016.7886668
Kenneth L. McMillan and Oded Padon
In: Lahiri, S., Wang, C. (eds) Computer Aided Verification. CAV 2020.
Lecture Notes in Computer Science(), vol 12225. Springer, Cham.
pp. 190–202, 2020.
external link https://doi.org/10.1007/978-3-030-53291-8_12
James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, Sharon Shoham
CAV 2024
external link zenodo artifact code: https://github.com/wilcoxjay/mypyvy
Oded Padon
Ph.D. Thesis
School of Computer Science, Tel Aviv University, Israel. 2019.
external link
Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham
Abstract
We develop a new technique for verifying temporal properties of infinite-state (distributed) systems. The main idea is to reduce the temporal verification problem to the problem of verifying the safety of infinite-state systems expressed in first-order logic. This allows to leverage existing techniques for safety verification to verify temporal properties of interesting distributed protocols, including some that have not been mechanically verified before.
We model infinite-state systems using first-order logic, and use first-order temporal logic (FO-LTL) to specify temporal properties. This general formalism allows to naturally model distributed systems, while supporting both unbounded-parallelism (where the system is allowed to dynamically create processes), and infinite-state per process.
The traditional approach for verifying temporal properties of infinite-state systems employs well-founded relations (e.g. using linear arithmetic ranking functions). In contrast, our approach is based the idea of fair cycle detection. In finite-state systems, temporal verification can always be reduced to fair cycle detection (a system contains a fair cycle if it revisits a state after satisfying all fairness constraints). However, with both infinitely many states and infinitely many fairness constraints, a straightforward reduction to fair cycle detection is unsound. To regain soundness, we augment the infinite-state transition system by a dynamically computed finite set, that exploits the locality of transitions. This set lets us define a form of fair cycle detection that is sound in the presence of both infinitely many states, and infinitely many fairness constraints. Our approach allows a new style of temporal verification that does not explicitly involve ranking functions. This fits well with pure first order verification which does not explicitly reason about numerical values. In particular, it can be used with effectively propositional first-order logic (EPR), and thus guaranteeing that checking inductiveness is decidable.
We applied our technique to verify temporal properties of several interesting protocols. To the best of our knowledge, we have obtained the first mechanized liveness proof for both TLB Shootdown, and Stoppable Paxos.
Modularity for decidability of deductive verification with applications to distributed systems.
PLDI 2018
In: Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Philadelphia, PA (2018)
external link
Kenneth L. McMillan, Oded Padon
SAS 2018
external link
Talks
ETAPS 2017
Invited tutorial
Tutorial talk given by Kenneth McMillan. (jea: this is one of the best introductions to start with).
Abstract
While full formal proof of complex systems remains a challenge, formal methods can readily be applied in practice to improve the performance of testing in exposing design errors. A good example of this is compositional testing. In this methodology, each component of a system is given a formal specification and it is proved formally that these specifications guarantee system-level correctness. The components are then rigorously tested against their formal specifications. This approach has the advantages of unit testing in covering component behaviors, while at the same time exposing all system-level errors to testing. Moreover, it can expose latent bugs in components that are not stimulated in the given system but may occur when the component is re-used in a different environment. This tutorial will cover the basics of compositional testing by example, introducing the available tools, and will also discuss industrial applications.
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Splash Conference 2017
Abstract
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, checking invariants of such protocols is undecidable and hard in practice, as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions and invariants involve higher-order concepts such as set cardinalities, arithmetic, and complex quantification.
This paper makes a step towards automatic verification of such protocols. We aim at a technique that can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order logic (also known as the Bernays-Schonfinkel-Ramsey class). In addition to decidability, EPR also enjoys the finite model property, allowing to display violations as finite structures which are intuitive for users. Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method. We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos, Vertical Paxos, Fast Paxos and Flexible Paxos. To the best of our knowledge, this work is the first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos and Fast Paxos.
Sep 13, 2018
The invited tutorial talk "Deductive Verification in Decidable Fragments with Ivy" was given by Kenneth L. McMillan and Oded Padon at the Static Analysis Symposium (SAS) 2018.
(Oded Padon, Weizmann Institute)
Oded Padon
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
Abstract: Many invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We present a new formal duality between states and predicates, and use it to derive a new primal-dual invariant inference algorithm. The new induction duality is based on a notion of provability by incremental induction that is formally dual to reachability, and the duality is surprisingly symmetric. The symmetry allows us to derive the dual of the well-known Houdini algorithm, and by combining Houdini with its dual image we obtain primal-dual Houdini, the first truly primal-dual invariant inference algorithm. An early prototype of primal-dual Houdini for the domain of distributed protocol verification can handle difficult benchmarks from the literature.
slides
Oded Padon
VMware Research
Tutorial at FMCAD 2022