LIPIcs.DISC.2021.48.pdf
- Filesize: 493 kB
- 4 pages
Document
Brief Announcement: Automating and Mechanising Cutoff Proofs for Parameterized Verification of Distributed Protocols
Authors
-
Part of:
Volume:
35th International Symposium on Distributed Computing (DISC 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Distributed Computing (DISC) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-10-04
Cite As Get BibTex
Shreesha G. Bhat and Kartik Nagar. Brief Announcement: Automating and Mechanising Cutoff Proofs for Parameterized Verification of Distributed Protocols. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 48:1-48:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.DISC.2021.48
Abstract
We propose a framework to automate and mechanize simulation-based proofs of cutoffs for parameterized verification of distributed protocols. We propose a strategy to derive the simulation relation given the cutoff instance and encode the correctness of the simulation relation as a formula in first-order logic. We have successfully applied our approach on a number of distributed protocols.
Subject Classification
ACM Subject Classification
- Software and its engineering → Software verification
Keywords
- Formal Methods
- Automated Verification
- Distributed Protocols
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.
-
Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008.
-
E. Allen Emerson and Kedar S. Namjoshi. Reasoning about rings. In POPL, pages 85-94. ACM Press, 1995.
-
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, and Mooly Sagiv. Inferring inductive invariants from phase structures. In CAV (2), volume 11562 of Lecture Notes in Computer Science, pages 405-425. Springer, 2019.
-
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. Ironfleet: proving practical distributed systems correct. In SOSP, pages 1-17. ACM, 2015.
-
Nouraldin Jaber, Swen Jacobs, Christopher Wagner, Milind Kulkarni, and Roopsha Samanta. Parameterized verification of systems with global synchronization and guards. In CAV (1), volume 12224 of Lecture Notes in Computer Science, pages 299-323. Springer, 2020.
-
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A. Sakallah. I4: incremental inference of inductive invariants for verification of distributed protocols. In SOSP, pages 370-384. ACM, 2019.
-
Ognjen Maric, Christoph Sprenger, and David A. Basin. Cutoff bounds for consensus algorithms. In CAV (2), volume 10427 of Lecture Notes in Computer Science, pages 217-237. Springer, 2017.
-
Kenneth L. McMillan and Oded Padon. Ivy: A multi-modal verification tool for distributed algorithms. In CAV (2), volume 12225 of Lecture Notes in Computer Science, pages 190-202. Springer, 2020.
-
Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang., 1(OOPSLA):108:1-108:31, 2017.
-
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. In PLDI, pages 614-630. ACM, 2016.
-
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. Modularity for decidability of deductive verification with applications to distributed systems. In PLDI, pages 662-677. ACM, 2018.
-
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas E. Anderson. Verdi: a framework for implementing and formally verifying distributed systems. In PLDI, pages 357-368. ACM, 2015.