There's a wealth of additional information to read in and around Ivy:
YouTube talks:
- SAS 2018 - Deductive Verification in Decidable Fragments with Ivy (by Ken McMillan, Oded Padon) youtube
- SAS 2018 - Interactive Verification of Distributed Protocols using Decidable Logic (by Sharon Shoham) youtube
- PLDI 2018 - Modularity for Decidability of Deductive Verification with Applications to Distributed Systems (by Marcelo Taube) youtube
- PLDI 2016 - Ivy: Safety Verification by Interactive Generalization (by Oded Padon) youtube
Papers
- CAV 2020 - Ivy: A Multi-modal Verification Tool for Distributed Algorithms (by Ken McMillan and Oded Padon) html
- SAS 2018 - Deductive Verification in Decidable Fragments with Ivy (by Ken McMillan and Oded Padon) pdf
- PLDI 2018 - Modularity for Decidability of Deductive Verification with Applications to Distributed Systems (by Marcelo Taube, Giuliano Losa, Ken McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, Doug Woos) pdf
- PLDI 2016 - Ivy: Safety Verification by Interactive Generalization (by Oded Padon, Ken McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham) pdf
- OOPSLA 2017 - Paxos Made EPR: Decidable Reasoning about Distributed Protocols (by Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham)pdf
- POPL 2018 - Reducing Liveness to Safety in First-Order Logic (by Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham) (pdf
- CAV 2009 - Complete instantiation for quantified formulas in Satisfiability Modulo Theories (by Leonardo de Moura and Yeting Ge) pdf
- LPAR 2007 - Decidable Fragments of Many-Sorted Logic (by Ahaon Abadi, Alexander Rabinovich and Mooly Sagiv) pdf
- TOPLAS 1983 - Tentative Steps Toward a Development Method for Interfering Programs (by C. B. Jones) -- origin of "rely-guarantee reasoning" pdf
Thesis
- Oded Padon, 2018: Deductive verification of distributed protocols in first-order logic pdf