• Baumeister T, Eichler P, Jacobs S, Sakr M and Völp M. (2025). Parameterized Verification of Round-Based Distributed Algorithms via Extended Threshold Automata. Formal Methods. 10.1007/978-3-031-71162-6_33. (638-657).

    https://link.springer.com/10.1007/978-3-031-71162-6_33

  • Gao S, Zhan B, Wu Z and Zhang L. (2024). Verifying Randomized Consensus Protocols with Common Coins 2024 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). 10.1109/DSN58291.2024.00047. 979-8-3503-4105-8. (403-415).

    https://ieeexplore.ieee.org/document/10647004/

  • Tamir O, Taube M, McMillan K, Shoham S, Howell J, Gueta G and Sagiv M. (2023). Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. Proceedings of the ACM on Programming Languages. 7:OOPSLA2. (1878-1904). Online publication date: 16-Oct-2023.

    https://doi.org/10.1145/3622864

  • Thomas B and Sankur O. PyLTA: A Verification Tool for Parameterized Distributed Algorithms. Tools and Algorithms for the Construction and Analysis of Systems. (28-35).

    https://doi.org/10.1007/978-3-031-30820-8_4

  • Feldman Y, Sagiv M, Shoham S and Wilcox J. (2022). Property-directed reachability as abstract interpretation in the monotone theory. Proceedings of the ACM on Programming Languages. 6:POPL. (1-31). Online publication date: 16-Jan-2022.

    https://doi.org/10.1145/3498676

  • Li J, Hu K, Zhu J, Bodeveix J, Ye Y and Han J. (2022). Formal Modelling of PBFT Consensus Algorithm in Event-B. Wireless Communications & Mobile Computing. 2022. Online publication date: 1-Jan-2022.

    https://doi.org/10.1155/2022/4467917

  • Viering M, Hu R, Eugster P and Ziarek L. (2021). A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proceedings of the ACM on Programming Languages. 5:OOPSLA. (1-30). Online publication date: 20-Oct-2021.

    https://doi.org/10.1145/3485501

  • Moloodi H, Faghih F and Bonakdarpour B. (2021). Parameterized Distributed Synthesis of Fault-Tolerance Using Counter Abstraction 2021 40th International Symposium on Reliable Distributed Systems (SRDS). 10.1109/SRDS53918.2021.00016. 978-1-6654-3819-3. (67-77).

    https://ieeexplore.ieee.org/document/9603553/

  • Crain T, Natoli C and Gramoli V. (2021). Red Belly: A Secure, Fair and Scalable Open Blockchain 2021 IEEE Symposium on Security and Privacy (SP). 10.1109/SP40001.2021.00087. 978-1-7281-8934-5. (466-483).

    https://ieeexplore.ieee.org/document/9519440/

  • Stoilkovska I, Konnov I, Widder J and Zuleger F. Eliminating Message Counters in Threshold Automata. Automated Technology for Verification and Analysis. (196-212).

    https://doi.org/10.1007/978-3-030-59152-6_11

  • Griffin J, Lesani M, Shadab N and Yin X. (2020). TLC: temporal logic of distributed components. Proceedings of the ACM on Programming Languages. 4:ICFP. (1-30). Online publication date: 2-Aug-2020.

    https://doi.org/10.1145/3409005

  • Klinkhamer A and Ebnenasir A. (2019). On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings. ACM Transactions on Computational Logic. 20:3. (1-36). Online publication date: 31-Jul-2019.

    https://doi.org/10.1145/3326456

  • v. Gleissenthall K, Kıcı R, Bakst A, Stefan D and Jhala R. (2019). Pretend synchrony: synchronous verification of asynchronous distributed programs. Proceedings of the ACM on Programming Languages. 3:POPL. (1-30). Online publication date: 2-Jan-2019.

    https://doi.org/10.1145/3290372

  • Berkovits I, Lazić M, Losa G, Padon O and Shoham S. (2019). Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. Computer Aided Verification. 10.1007/978-3-030-25543-5_15. (245-266).

    http://link.springer.com/10.1007/978-3-030-25543-5_15

  • Taube M, Losa G, McMillan K, Padon O, Sagiv M, Shoham S, Wilcox J and Woos D. (2018). Modularity for decidability of deductive verification with applications to distributed systems. ACM SIGPLAN Notices. 53:4. (662-677). Online publication date: 2-Dec-2018.

    https://doi.org/10.1145/3296979.3192414

  • Taube M, Losa G, McMillan K, Padon O, Sagiv M, Shoham S, Wilcox J and Woos D. Modularity for decidability of deductive verification with applications to distributed systems. Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. (662-677).

    https://doi.org/10.1145/3192366.3192414

  • Padon O, Hoenicke J, Losa G, Podelski A, Sagiv M and Shoham S. (2017). Reducing liveness to safety in first-order logic. Proceedings of the ACM on Programming Languages. 2:POPL. (1-33). Online publication date: 1-Jan-2018.

    https://doi.org/10.1145/3158114

  • Shoham S. (2018). Interactive Verification of Distributed Protocols Using Decidable Logic. Static Analysis. 10.1007/978-3-319-99725-4_7. (77-85).

    http://link.springer.com/10.1007/978-3-319-99725-4_7

  • Aminof B, Rubin S, Stoilkovska I, Widder J and Zuleger F. (2018). Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction. Verification, Model Checking, and Abstract Interpretation. 10.1007/978-3-319-73721-8_1. (1-24).

    http://link.springer.com/10.1007/978-3-319-73721-8_1

  • Konnov I, Lazić M, Veith H and Widder J. (2017). Para$$^2$$2. Formal Methods in System Design. 51:2. (270-307). Online publication date: 1-Nov-2017.

    https://doi.org/10.1007/s10703-017-0297-4

  • Padon O, Losa G, Sagiv M and Shoham S. (2017). Paxos made EPR: decidable reasoning about distributed protocols. Proceedings of the ACM on Programming Languages. 1:OOPSLA. (1-31). Online publication date: 12-Oct-2017.

    https://doi.org/10.1145/3140568

  • Konnov I, Lazić M, Veith H and Widder J. (2017). A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. ACM SIGPLAN Notices. 52:1. (719-734). Online publication date: 11-May-2017.

    https://doi.org/10.1145/3093333.3009860

  • Konnov I, Widder J, Spegni F and Spalazzi L. (2017). Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms. Verification, Model Checking, and Abstract Interpretation. 10.1007/978-3-319-52234-0_19. (347-366).

    http://link.springer.com/10.1007/978-3-319-52234-0_19

  • Jaber N, Wagner C, Jacobs S, Kulkarni M and Samanta R. Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification. Tools and Algorithms for the Construction and Analysis of Systems. (289-308).

    https://doi.org/10.1007/978-3-031-30820-8_19

  • Chini P, Meyer R and Saivasan P. (2021). Liveness in broadcast networks. Computing. 10.1007/s00607-021-00986-y. 104:10. (2203-2223). Online publication date: 1-Oct-2022.

    https://link.springer.com/10.1007/s00607-021-00986-y

  • Stoilkovska I, Konnov I, Widder J and Zuleger F. (2021). Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. International Journal on Software Tools for Technology Transfer. 10.1007/s10009-021-00637-9. 24:1. (33-48). Online publication date: 1-Feb-2022.

    https://link.springer.com/10.1007/s10009-021-00637-9

  • Balasubramanian A. (2022). Coefficient Synthesis for Threshold Automata. Reachability Problems. 10.1007/978-3-031-19135-0_9. (125-139).

    https://link.springer.com/10.1007/978-3-031-19135-0_9

  • Tholoniat P and Gramoli V. (2022). Formal Verification of Blockchain Byzantine Fault Tolerance. Handbook on Blockchain. 10.1007/978-3-031-07535-3_12. (389-412).

    https://link.springer.com/10.1007/978-3-031-07535-3_12

  • Bertrand N, Konnov I, Lazić M and Widder J. (2021). Verification of randomized consensus algorithms under round-rigid adversaries. International Journal on Software Tools for Technology Transfer. 10.1007/s10009-020-00603-x.

    https://link.springer.com/10.1007/s10009-020-00603-x

  • Tran T, Konnov I and Widder J. (2021). A Case Study on Parametric Verification of Failure Detectors. Formal Techniques for Distributed Objects, Components, and Systems. 10.1007/978-3-030-78089-0_8. (138-156).

    https://link.springer.com/10.1007/978-3-030-78089-0_8

  • Bertrand N, Lazić M and Widder J. (2021). A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries. Verification, Model Checking, and Abstract Interpretation. 10.1007/978-3-030-67067-2_11. (219-239).

    http://link.springer.com/10.1007/978-3-030-67067-2_11

  • Stoilkovska I, Konnov I, Widder J and Zuleger F. (2021). Eliminating Message Counters in Synchronous Threshold Automata. Verification, Model Checking, and Abstract Interpretation. 10.1007/978-3-030-67067-2_10. (196-218).

    http://link.springer.com/10.1007/978-3-030-67067-2_10

  • Jaber N, Jacobs S, Wagner C, Kulkarni M and Samanta R. Parameterized Verification of Systems with Global Synchronization and Guards. Computer Aided Verification. (299-323).

    https://doi.org/10.1007/978-3-030-53288-8_15

  • Konnov I, Lazić M, Stoilkovska I and Widder J. (2020). Tutorial: Parameterized Verification with Byzantine Model Checker. Formal Techniques for Distributed Objects, Components, and Systems. 10.1007/978-3-030-50086-3_11. (189-207).

    http://link.springer.com/10.1007/978-3-030-50086-3_11

  • Konnov I, Kukovec J and Tran T. (2019). TLA+ model checking made symbolic. Proceedings of the ACM on Programming Languages. 3:OOPSLA. (1-30). Online publication date: 10-Oct-2019.

    https://doi.org/10.1145/3360549

  • Klinkhamer A and Ebnenasir A. (2019). On the Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings. ACM Transactions on Computational Logic. 20:3. (1-36). Online publication date: 31-Jul-2019.

    https://doi.org/10.1145/3326456

  • Chini P, Meyer R and Saivasan P. (2019). Liveness in Broadcast Networks. Networked Systems. 10.1007/978-3-030-31277-0_4. (52-66).

    http://link.springer.com/10.1007/978-3-030-31277-0_4

  • Damian A, Drăgoi C, Militaru A and Widder J. (2019). Communication-Closed Asynchronous Protocols. Computer Aided Verification. 10.1007/978-3-030-25543-5_20. (344-363).

    http://link.springer.com/10.1007/978-3-030-25543-5_20

  • Stoilkovska I, Konnov I, Widder J and Zuleger F. (2019). Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. Tools and Algorithms for the Construction and Analysis of Systems. 10.1007/978-3-030-17465-1_20. (357-374).

    http://link.springer.com/10.1007/978-3-030-17465-1_20

  • Kukovec J, Tran T and Konnov I. (2018). Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications. Abstract State Machines, Alloy, B, TLA, VDM, and Z. 10.1007/978-3-319-91271-4_7. (89-104).

    http://link.springer.com/10.1007/978-3-319-91271-4_7

  • Rahli V, Vukotic I, Völp M and Esteves-Verissimo P. (2018). Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. Programming Languages and Systems. 10.1007/978-3-319-89884-1_22. (619-650).

    http://link.springer.com/10.1007/978-3-319-89884-1_22

  • Konnov I and Widder J. (2018). ByMC: Byzantine Model Checker. Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. 10.1007/978-3-030-03424-5_22. (327-342).

    http://link.springer.com/10.1007/978-3-030-03424-5_22