Document Open Access Logo

Brief Announcement: Automating and Mechanising Cutoff Proofs for Parameterized Verification of Distributed Protocols

Authors Shreesha G. Bhat, Kartik Nagar

Thumbnail PDF


  • Filesize: 493 kB
  • 4 pages

Document Identifiers

Author Details

Shreesha G. Bhat
  • Indian Institute of Technology Madras, India
Kartik Nagar
  • Indian Institute of Technology Madras, India

Cite AsGet 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)


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
  • Formal Methods
  • Automated Verification
  • Distributed Protocols


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. 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. Google Scholar
  2. 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. Google Scholar
  3. E. Allen Emerson and Kedar S. Namjoshi. Reasoning about rings. In POPL, pages 85-94. ACM Press, 1995. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail