references.bib

@article{konnov2017iandc,
  author       = {Igor V. Konnov and
                  Helmut Veith and
                  Josef Widder},
  title        = {On the completeness of bounded model checking for threshold-based
                  distributed algorithms: Reachability},
  journal      = {Inf. Comput.},
  volume       = {252},
  pages        = {95--109},
  year         = {2017},
  url          = {https://doi.org/10.1016/j.ic.2016.03.006},
  doi          = {10.1016/J.IC.2016.03.006},
  timestamp    = {Tue, 04 Feb 2020 18:05:55 +0100},
  biburl       = {https://dblp.org/rec/journals/iandc/KonnovVW17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@misc{bala2020complexity,
      title={Complexity of Verification and Synthesis of Threshold Automata}, 
      author={A. R. Balasubramanian and Javier Esparza and Marijana Lazic},
      year={2020},
      eprint={2007.06248},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      url={https://arxiv.org/abs/2007.06248}, 
}

@article{konnov2016corr,
  author       = {Igor Konnov and
                  Marijana Lazic and
                  Helmut Veith and
                  Josef Widder},
  title        = {A Short Counterexample Property for Safety and Liveness Verification
                  of Fault-tolerant Distributed Algorithms},
  journal      = {CoRR},
  volume       = {abs/1608.05327},
  year         = {2016},
  url          = {http://arxiv.org/abs/1608.05327},
  eprinttype    = {arXiv},
  eprint       = {1608.05327},
  timestamp    = {Sat, 23 Jan 2021 01:20:12 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/KonnovLVW16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@misc{lamport1992distributed,
  author    = {Lamport, Leslie},
  publisher = {June},
  title     = {A distributed system is one in which the failure of a computer you didn't even know existed can render your own computer unusable." {\'a} CACM},
  year      = {1992},
  url = {https://lamport.azurewebsites.net/pubs/distributed-system.txt}
}

@inproceedings{OngaroO14,
  author       = {Diego Ongaro and
                  John K. Ousterhout},
  editor       = {Garth Gibson and
                  Nickolai Zeldovich},
  title        = {In Search of an Understandable Consensus Algorithm},
  booktitle    = {Proceedings of the 2014 {USENIX} Annual Technical Conference, {USENIX}
                  {ATC} 2014, Philadelphia, PA, USA, June 19-20, 2014},
  pages        = {305--319},
  publisher    = {{USENIX} Association},
  year         = {2014},
  url          = {https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro},
  timestamp    = {Tue, 16 Jul 2024 09:12:32 +0200},
  biburl       = {https://dblp.org/rec/conf/usenix/OngaroO14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{LamportSP82,
  author       = {Leslie Lamport and
                  Robert E. Shostak and
                  Marshall C. Pease},
  title        = {The Byzantine Generals Problem},
  journal      = {{ACM} Trans. Program. Lang. Syst.},
  volume       = {4},
  number       = {3},
  pages        = {382--401},
  year         = {1982},
  url          = {https://doi.org/10.1145/357172.357176},
  doi          = {10.1145/357172.357176},
  timestamp    = {Fri, 24 Mar 2023 16:31:07 +0100},
  biburl       = {https://dblp.org/rec/journals/toplas/LamportSP82.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{PirleaGKZS25,
  author       = {George P{\^{\i}}rlea and
                  Vladimir Gladshtein and
                  Elad Kinsbruner and
                  Qiyuan Zhao and
                  Ilya Sergey},
  editor       = {Ruzica Piskac and
                  Zvonimir Rakamaric},
  title        = {Veil: {A} Framework for Automated and Interactive Verification of
                  Transition Systems},
  booktitle    = {Computer Aided Verification - 37th International Conference, {CAV}
                  2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part {III}},
  series       = {Lecture Notes in Computer Science},
  volume       = {15933},
  pages        = {26--41},
  publisher    = {Springer},
  year         = {2025},
  url          = {https://doi.org/10.1007/978-3-031-98682-6_2},
  doi          = {10.1007/978-3-031-98682-6_2},
  timestamp    = {Sat, 09 Aug 2025 12:14:22 +0200},
  biburl       = {https://dblp.org/rec/conf/cav/PirleaGKZS25.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{holistic,
  title={Holistic verification of blockchain consensus},
  author={Bertrand, Nathalie and Gramoli, Vincent and Konnov, Igor and Lazi{\'c}, Marijana and Tholoniat, Pierre and Widder, Josef},
  journal={arXiv preprint arXiv:2206.04489},
  year={2022}
}
@article{BrachaT85,
  author       = {Gabriel Bracha and
                  Sam Toueg},
  title        = {Asynchronous Consensus and Broadcast Protocols},
  journal      = {J. {ACM}},
  volume       = {32},
  number       = {4},
  pages        = {824--840},
  year         = {1985},
  url          = {https://doi.org/10.1145/4221.214134},
  doi          = {10.1145/4221.214134},
  timestamp    = {Sun, 19 Jan 2025 14:36:57 +0100},
  biburl       = {https://dblp.org/rec/journals/jacm/BrachaT85.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{MostefaouiMPR03,
  author       = {Achour Most{\'{e}}faoui and
                  Eric Mourgaya and
                  Philippe Raipin Parv{\'{e}}dy and
                  Michel Raynal},
  title        = {Evaluating the Condition-Based Approach to Solve Consensus},
  booktitle    = {2003 International Conference on Dependable Systems and Networks {(DSN}
                  2003), 22-25 June 2003, San Francisco, CA, USA, Proceedings},
  pages        = {541--550},
  publisher    = {{IEEE} Computer Society},
  year         = {2003},
  url          = {https://doi.org/10.1109/DSN.2003.1209964},
  doi          = {10.1109/DSN.2003.1209964},
  timestamp    = {Fri, 24 Mar 2023 00:01:47 +0100},
  biburl       = {https://dblp.org/rec/conf/dsn/MostefaouiMPR03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{BrasileiroGMR01,
  author       = {Francisco Vilar Brasileiro and
                  Fab{\'{\i}}ola Greve and
                  Achour Most{\'{e}}faoui and
                  Michel Raynal},
  editor       = {Victor E. Malyshkin},
  title        = {Consensus in One Communication Step},
  booktitle    = {Parallel Computing Technologies, 6th International Conference, PaCT
                  2001, Novosibirsk, Russia, September 3-7, 2001, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2127},
  pages        = {42--50},
  publisher    = {Springer},
  year         = {2001},
  url          = {https://doi.org/10.1007/3-540-44743-1_4},
  doi          = {10.1007/3-540-44743-1_4},
  timestamp    = {Mon, 03 Mar 2025 21:19:40 +0100},
  biburl       = {https://dblp.org/rec/conf/pact/BrasileiroGMR01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{ThomasS23,
  author       = {Bastien Thomas and
                  Ocan Sankur},
  editor       = {Sriram Sankaranarayanan and
                  Natasha Sharygina},
  title        = {PyLTA: {A} Verification Tool for Parameterized Distributed Algorithms},
  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems
                  - 29th International Conference, {TACAS} 2023, Held as Part of the
                  European Joint Conferences on Theory and Practice of Software, {ETAPS}
                  2022, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13994},
  pages        = {28--35},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-30820-8_4},
  doi          = {10.1007/978-3-031-30820-8_4},
  timestamp    = {Sat, 13 May 2023 01:07:18 +0200},
  biburl       = {https://dblp.org/rec/conf/tacas/ThomasS23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{barrett2010smt,
  title={The {SMT-LIB} standard: Version 2.0},
  author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare and others},
  booktitle={Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK)},
  volume={13},
  pages={14},
  year={2010}
}

@article{rackoff1978covering,
  title={The covering and boundedness problems for vector addition systems},
  author={Rackoff, Charles},
  journal={Theoretical Computer Science},
  volume={6},
  number={2},
  pages={223--231},
  year={1978},
  publisher={Elsevier}
}
@inproceedings{Finkel91,
  author       = {Alain Finkel},
  title        = {The Minimal Coverability Graph for Petri Nets},
  booktitle    = {Applications and Theory of Petri Nets},
  series       = {Lecture Notes in Computer Science},
  volume       = {674},
  pages        = {210--243},
  publisher    = {Springer},
  year         = {1991}
}
@article{bdds,
  title={Binary decision diagrams},
  author={Akers},
  journal={IEEE Transactions on computers},
  volume={100},
  number={6},
  pages={509--516},
  year={1978},
  publisher={IEEE}
}
@article{wsts,
  title={Well-structured transition systems everywhere!},
  author={Finkel, Alain and Schnoebelen, Ph},
  journal={Theoretical Computer Science},
  volume={256},
  number={1-2},
  pages={63--92},
  year={2001},
  publisher={Elsevier}
}
@article{srikanth1987simulating,
  title={Simulating authenticated broadcasts to derive simple fault-tolerant algorithms},
  author={Srikanth, TK and Toueg, Sam},
  journal={Distributed Computing},
  volume={2},
  number={2},
  pages={80--94},
  year={1987},
  publisher={Springer}
}

@inproceedings{Balasubramanian20,
  author       = {A. R. Balasubramanian and
                  Javier Esparza and
                  Marijana Lazic},
  editor       = {Dang Van Hung and
                  Oleg Sokolsky},
  title        = {Complexity of Verification and Synthesis of Threshold Automata},
  booktitle    = {Automated Technology for Verification and Analysis - 18th International
                  Symposium, {ATVA} 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12302},
  pages        = {144--160},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-59152-6_8},
  doi          = {10.1007/978-3-030-59152-6_8},
  timestamp    = {Tue, 20 Oct 2020 18:27:30 +0200},
  biburl       = {https://dblp.org/rec/conf/atva/Balasubramanian20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{KW18,
  author       = {Igor Konnov and
                  Josef Widder},
  editor       = {Tiziana Margaria and
                  Bernhard Steffen},
  title        = {ByMC: Byzantine Model Checker},
  booktitle    = {Leveraging Applications of Formal Methods, Verification and Validation.
                  Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol,
                  Cyprus, November 5-9, 2018, Proceedings, Part {III}},
  series       = {Lecture Notes in Computer Science},
  volume       = {11246},
  pages        = {327--342},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-030-03424-5_22},
  doi          = {10.1007/978-3-030-03424-5_22},
  timestamp    = {Sat, 05 Sep 2020 17:55:57 +0200},
  biburl       = {https://dblp.org/rec/conf/isola/0001W18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{KLSW23,
  author       = {Igor Konnov and
                  Marijana Lazic and
                  Ilina Stoilkovska and
                  Josef Widder},
  title        = {Survey on Parameterized Verification with Threshold Automata and the
                  Byzantine Model Checker},
  journal      = {Log. Methods Comput. Sci.},
  volume       = {19},
  number       = {1},
  year         = {2023},
  url          = {https://doi.org/10.46298/lmcs-19(1:5)2023},
  doi          = {10.46298/LMCS-19(1:5)2023},
  timestamp    = {Sat, 30 Sep 2023 10:20:49 +0200},
  biburl       = {https://dblp.org/rec/journals/lmcs/0001LSW23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{BaumeisterEJSV24,
  author       = {Tom Baumeister and
                  Paul Eichler and
                  Swen Jacobs and
                  Mouhammad Sakr and
                  Marcus V{\"{o}}lp},
  editor       = {Andr{\'{e}} Platzer and
                  Kristin Yvonne Rozier and
                  Matteo Pradella and
                  Matteo Rossi},
  title        = {Parameterized Verification of Round-Based Distributed Algorithms via
                  Extended Threshold Automata},
  booktitle    = {Formal Methods - 26th International Symposium, {FM} 2024, Milan, Italy,
                  September 9-13, 2024, Proceedings, Part {I}},
  series       = {Lecture Notes in Computer Science},
  volume       = {14933},
  pages        = {638--657},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-71162-6_33},
  doi          = {10.1007/978-3-031-71162-6_33},
  timestamp    = {Mon, 09 Dec 2024 22:46:03 +0100},
  biburl       = {https://dblp.org/rec/conf/fm/BaumeisterEJSV24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{KonnovVW14,
  author       = {Igor Konnov and
                  Helmut Veith and
                  Josef Widder},
  editor       = {Paolo Baldan and
                  Daniele Gorla},
  title        = {On the Completeness of Bounded Model Checking for Threshold-Based
                  Distributed Algorithms: Reachability},
  booktitle    = {{CONCUR} 2014 - Concurrency Theory - 25th International Conference,
                  {CONCUR} 2014, Rome, Italy, September 2-5, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8704},
  pages        = {125--140},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-44584-6_10},
  doi          = {10.1007/978-3-662-44584-6_10},
  timestamp    = {Tue, 14 May 2019 10:00:43 +0200},
  biburl       = {https://dblp.org/rec/conf/concur/KonnovVW14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{KonnovVW15,
  author    = {Igor V. Konnov and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/ershov/KonnovVW15.bib},
  booktitle = {Perspectives of System Informatics - 10th International Andrei Ershov
               Informatics Conference, {PSI} 2015, in Memory of Helmut Veith, Kazan
               and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers},
  doi       = {10.1007/978-3-319-41579-6_2},
  editor    = {Manuel Mazzara and
               Andrei Voronkov},
  pages     = {6--21},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Sun, 02 Jun 2019 21:19:59 +0200},
  title     = {What You Always Wanted to Know About Model Checking of Fault-Tolerant
               Distributed Algorithms},
  url       = {https://doi.org/10.1007/978-3-319-41579-6_2},
  volume    = {9609},
  year      = {2015}
}


@inproceedings{KonnovLVW17,
  author       = {Igor V. Konnov and
                  Marijana Lazic and
                  Helmut Veith and
                  Josef Widder},
  editor       = {Giuseppe Castagna and
                  Andrew D. Gordon},
  title        = {A short counterexample property for safety and liveness verification
                  of fault-tolerant distributed algorithms},
  booktitle    = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
                  Programming Languages, {POPL} 2017, Paris, France, January 18-20,
                  2017},
  pages        = {719--734},
  publisher    = {{ACM}},
  year         = {2017},
  url          = {https://doi.org/10.1145/3009837.3009860},
  doi          = {10.1145/3009837.3009860},
  timestamp    = {Sun, 19 Jan 2025 13:36:33 +0100},
  biburl       = {https://dblp.org/rec/conf/popl/KonnovLVW17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Kukovec0W18,
  author       = {Jure Kukovec and
                  Igor Konnov and
                  Josef Widder},
  editor       = {Sven Schewe and
                  Lijun Zhang},
  title        = {Reachability in Parameterized Systems: All Flavors of Threshold Automata},
  booktitle    = {29th International Conference on Concurrency Theory, {CONCUR} 2018,
                  September 4-7, 2018, Beijing, China},
  series       = {LIPIcs},
  volume       = {118},
  pages        = {19:1--19:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2018},
  url          = {https://doi.org/10.4230/LIPIcs.CONCUR.2018.19},
  doi          = {10.4230/LIPICS.CONCUR.2018.19},
  timestamp    = {Sat, 05 Sep 2020 18:00:10 +0200},
  biburl       = {https://dblp.org/rec/conf/concur/Kukovec0W18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{BertrandKLW19,
  author       = {Nathalie Bertrand and
                  Igor Konnov and
                  Marijana Lazic and
                  Josef Widder},
  editor       = {Wan J. Fokkink and
                  Rob van Glabbeek},
  title        = {Verification of Randomized Consensus Algorithms Under Round-Rigid
                  Adversaries},
  booktitle    = {30th International Conference on Concurrency Theory, {CONCUR} 2019,
                  August 27-30, 2019, Amsterdam, the Netherlands},
  series       = {LIPIcs},
  volume       = {140},
  pages        = {33:1--33:15},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2019},
  url          = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.33},
  doi          = {10.4230/LIPICS.CONCUR.2019.33},
  timestamp    = {Wed, 21 Aug 2024 22:46:00 +0200},
  biburl       = {https://dblp.org/rec/conf/concur/BertrandKLW19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Stoilkovska0WZ20,
  author       = {Ilina Stoilkovska and
                  Igor Konnov and
                  Josef Widder and
                  Florian Zuleger},
  editor       = {Dang Van Hung and
                  Oleg Sokolsky},
  title        = {Eliminating Message Counters in Threshold Automata},
  booktitle    = {Automated Technology for Verification and Analysis - 18th International
                  Symposium, {ATVA} 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12302},
  pages        = {196--212},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-59152-6_11},
  doi          = {10.1007/978-3-030-59152-6_11},
  timestamp    = {Tue, 13 Oct 2020 16:57:38 +0200},
  biburl       = {https://dblp.org/rec/conf/atva/Stoilkovska0WZ20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{StoilkovskaKWZ21,
  author       = {Ilina Stoilkovska and
                  Igor Konnov and
                  Josef Widder and
                  Florian Zuleger},
  editor       = {Fritz Henglein and
                  Sharon Shoham and
                  Yakir Vizel},
  title        = {Eliminating Message Counters in Synchronous Threshold Automata},
  booktitle    = {Verification, Model Checking, and Abstract Interpretation - 22nd International
                  Conference, {VMCAI} 2021, Copenhagen, Denmark, January 17-19, 2021,
                  Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12597},
  pages        = {196--218},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-67067-2_10},
  doi          = {10.1007/978-3-030-67067-2_10},
  timestamp    = {Wed, 13 Jan 2021 17:58:40 +0100},
  biburl       = {https://dblp.org/rec/conf/vmcai/StoilkovskaKWZ21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% I could not find more information on CUDD
@misc{cudd,
  author = {
    Fabio Somenzi and
    Iris Bahar and
    Hyunwoo Cho and 
    Erica Frohm and 
    Charlie Gaona and 
    Cheng Hua and 
    Jae-Young Jang and 
    Seh-Woong Jeong and 
    Balakrishna Kumthekar and
    Enrico Macii and  
    Bobbie Manne and 
    In-Ho Moon and
    Curt Musfeldt and 
    Shipra Panda and 
    Abelardo Pardo and 
    Bernard Plessier  
    Kavita Ravi and 
    Hyongkyoon Shin and 
    Alan Shuler and 
    Arun Sivakumaran and 
    Jorgen Sivesind},
  date = {unknown},
  url = {https://github.com/cuddorg/cudd},
  editor = {unkown},
  title = {CUDD: CU Decision Diagram Package},
  year = {unkown}
}


@inproceedings{cvc5,
  author    = {Haniel Barbosa and
               Clark W. Barrett and
               Martin Brain and
               Gereon Kremer and
               Hanna Lachnitt and
               Makai Mann and
               Abdalrhman Mohamed and
               Mudathir Mohamed and
               Aina Niemetz and
               Andres N{\"{o}}tzli and
               Alex Ozdemir and
               Mathias Preiner and
               Andrew Reynolds and
               Ying Sheng and
               Cesare Tinelli and
               Yoni Zohar},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 28th International Conference, {TACAS} 2022, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
  doi       = {10.1007/978-3-030-99524-9_24},
  editor    = {Dana Fisman and
               Grigore Rosu},
  pages     = {415--442},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Fri, 01 Apr 2022 15:49:27 +0200},
  title     = {cvc5: {A} Versatile and Industrial-Strength {SMT} Solver},
  url       = {https://doi.org/10.1007/978-3-030-99524-9_24},
  volume    = {13243},
  year      = {2022}
}

% Please keep the url in this entry
@inproceedings{z3,
  author    = {Leonardo Mendon{\c{c}}a de Moura and
               Nikolaj S. Bj{\o}rner},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
               14th International Conference, {TACAS} 2008, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2008,
               Budapest, Hungary, March 29-April 6, 2008. Proceedings},
  doi       = {10.1007/978-3-540-78800-3_24},
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  pages     = {337--340},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Mon, 03 Apr 2023 17:23:33 +0200},
  title     = {{Z3:} An Efficient {SMT} Solver},
  url       = {https://github.com/z3prover/z3}, 
  volume    = {4963},
  year      = {2008}
}

@inproceedings{oxidd24,
  author    = {Husung, Nils and Dubslaff, Clemens and Hermanns, Holger and K{\"o}hl, Maximilian A.},
  booktitle = {Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'24)},
  doi       = {10.1007/978-3-031-57256-2_13},
  title     = {{OxiDD}: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in {Rust}},
  year      = {2024}
}

@article{HawblitzelHKLPR17,
  author    = {Chris Hawblitzel and
               Jon Howell and
               Manos Kapritsos and
               Jacob R. Lorch and
               Bryan Parno and
               Michael Lowell Roberts and
               Srinath T. V. Setty and
               Brian Zill},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/cacm/HawblitzelHKLPR17.bib},
  doi       = {10.1145/3068608},
  journal   = {Commun. {ACM}},
  number    = {7},
  pages     = {83--92},
  timestamp = {Sun, 19 Jan 2025 14:03:26 +0100},
  title     = {IronFleet: proving safety and liveness of practical distributed systems},
  url       = {https://doi.org/10.1145/3068608},
  volume    = {60},
  year      = {2017}
}

@article{JaberWJKS21,
  author    = {Nouraldin Jaber and
               Christopher Wagner and
               Swen Jacobs and
               Milind Kulkarni and
               Roopsha Samanta},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/pacmpl/JaberWJKS21.bib},
  doi       = {10.1145/3485534},
  journal   = {Proc. {ACM} Program. Lang.},
  number    = {{OOPSLA}},
  pages     = {1--31},
  timestamp = {Sun, 19 Jan 2025 14:47:43 +0100},
  title     = {QuickSilver: modeling and parameterized verification for distributed
               agreement-based systems},
  url       = {https://doi.org/10.1145/3485534},
  volume    = {5},
  year      = {2021}
}

@inproceedings{McMillanP20,
  author    = {Kenneth L. McMillan and
               Oded Padon},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/cav/McMillanP20.bib},
  booktitle = {Computer Aided Verification - 32nd International Conference, {CAV}
               2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
  doi       = {10.1007/978-3-030-53291-8_12},
  editor    = {Shuvendu K. Lahiri and
               Chao Wang},
  pages     = {190--202},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Wed, 12 Aug 2020 15:15:44 +0200},
  title     = {Ivy: {A} Multi-modal Verification Tool for Distributed Algorithms},
  url       = {https://doi.org/10.1007/978-3-030-53291-8_12},
  volume    = {12225},
  year      = {2020}
}

@article{RahliGBC15,
  author    = {Vincent Rahli and
               David Guaspari and
               Mark Bickford and
               Robert L. Constable},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/eceasst/RahliGBC15.bib},
  doi       = {10.14279/TUJ.ECEASST.72.1013},
  journal   = {Electron. Commun. Eur. Assoc. Softw. Sci. Technol.},
  timestamp = {Tue, 25 Aug 2020 16:49:29 +0200},
  title     = {Formal Specification, Verification, and Implementation of Fault-Tolerant
               Systems using EventML},
  url       = {https://doi.org/10.14279/tuj.eceasst.72.1013},
  volume    = {72},
  year      = {2015}
}

@inproceedings{WilcoxWPTWEA15,
  author    = {James R. Wilcox and
               Doug Woos and
               Pavel Panchekha and
               Zachary Tatlock and
               Xi Wang and
               Michael D. Ernst and
               Thomas E. Anderson},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/pldi/WilcoxWPTWEA15.bib},
  booktitle = {Proceedings of the 36th {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation, Portland, OR, USA, June 15-17,
               2015},
  doi       = {10.1145/2737924.2737958},
  editor    = {David Grove and
               Stephen M. Blackburn},
  pages     = {357--368},
  publisher = {{ACM}},
  timestamp = {Sun, 19 Jan 2025 13:10:49 +0100},
  title     = {Verdi: a framework for implementing and formally verifying distributed
               systems},
  url       = {https://doi.org/10.1145/2737924.2737958},
  year      = {2015}
}

@inproceedings{CrainNG21,
  author    = {Tyler Crain and
               Christopher Natoli and
               Vincent Gramoli},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/sp/CrainNG21.bib},
  booktitle = {42nd {IEEE} Symposium on Security and Privacy, {SP} 2021, San Francisco,
               CA, USA, 24-27 May 2021},
  doi       = {10.1109/SP40001.2021.00087},
  pages     = {466--483},
  publisher = {{IEEE}},
  timestamp = {Thu, 21 Sep 2023 15:57:26 +0200},
  title     = {Red Belly: {A} Secure, Fair and Scalable Open Blockchain},
  url       = {https://doi.org/10.1109/SP40001.2021.00087},
  year      = {2021}
}


@inproceedings{JohnKSVW13,
  author    = {Annu John and
               Igor Konnov and
               Ulrich Schmid and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/fmcad/JohnKSVW13.bib},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2013, Portland, OR,
               USA, October 20-23, 2013},
  pages     = {201--209},
  publisher = {{IEEE}},
  timestamp = {Mon, 09 Aug 2021 15:21:44 +0200},
  title     = {Parameterized model checking of fault-tolerant distributed algorithms
               by abstraction},
  url       = {https://ieeexplore.ieee.org/document/6679411/},
  year      = {2013}
}

@inproceedings{GmeinerKSVW14,
  author    = {Annu Gmeiner and
               Igor Konnov and
               Ulrich Schmid and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/sfm/GmeinerKSVW14.bib},
  booktitle = {Formal Methods for Executable Software Models - 14th International
               School on Formal Methods for the Design of Computer, Communication,
               and Software Systems, {SFM} 2014, Bertinoro, Italy, June 16-20, 2014,
               Advanced Lectures},
  doi       = {10.1007/978-3-319-07317-0_4},
  editor    = {Marco Bernardo and
               Ferruccio Damiani and
               Reiner H{\"{a}}hnle and
               Einar Broch Johnsen and
               Ina Schaefer},
  pages     = {122--171},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Tue, 14 May 2019 10:00:44 +0200},
  title     = {Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed
               Algorithms},
  url       = {https://doi.org/10.1007/978-3-319-07317-0_4},
  volume    = {8483},
  year      = {2014}
}

@inproceedings{KonnovVW14,
  author    = {Igor Konnov and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/concur/KonnovVW14.bib},
  booktitle = {{CONCUR} 2014 - Concurrency Theory - 25th International Conference,
               {CONCUR} 2014, Rome, Italy, September 2-5, 2014. Proceedings},
  doi       = {10.1007/978-3-662-44584-6_10},
  editor    = {Paolo Baldan and
               Daniele Gorla},
  pages     = {125--140},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Tue, 14 May 2019 10:00:43 +0200},
  title     = {On the Completeness of Bounded Model Checking for Threshold-Based
               Distributed Algorithms: Reachability},
  url       = {https://doi.org/10.1007/978-3-662-44584-6_10},
  volume    = {8704},
  year      = {2014}
}

@article{KonnovVW17,
  author    = {Igor V. Konnov and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/iandc/KonnovVW17.bib},
  doi       = {10.1016/J.IC.2016.03.006},
  journal   = {Inf. Comput.},
  pages     = {95--109},
  timestamp = {Tue, 04 Feb 2020 18:05:55 +0100},
  title     = {On the completeness of bounded model checking for threshold-based
               distributed algorithms: Reachability},
  url       = {https://doi.org/10.1016/j.ic.2016.03.006},
  volume    = {252},
  year      = {2017}
}

@inproceedings{memKonnovVW15,
  author    = {Igor V. Konnov and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/ershov/KonnovVW15.bib},
  booktitle = {Perspectives of System Informatics - 10th International Andrei Ershov
               Informatics Conference, {PSI} 2015, in Memory of Helmut Veith, Kazan
               and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers},
  doi       = {10.1007/978-3-319-41579-6_2},
  editor    = {Manuel Mazzara and
               Andrei Voronkov},
  pages     = {6--21},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Sun, 02 Jun 2019 21:19:59 +0200},
  title     = {What You Always Wanted to Know About Model Checking of Fault-Tolerant
               Distributed Algorithms},
  url       = {https://doi.org/10.1007/978-3-319-41579-6_2},
  volume    = {9609},
  year      = {2015}
}

@inproceedings{KonnovVW15,
  author    = {Igor Konnov and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/cav/KonnovVW15.bib},
  booktitle = {Computer Aided Verification - 27th International Conference, {CAV}
               2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part
               {I}},
  doi       = {10.1007/978-3-319-21690-4_6},
  editor    = {Daniel Kroening and
               Corina S. Pasareanu},
  pages     = {85--102},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Fri, 27 Mar 2020 08:45:57 +0100},
  title     = {{SMT} and {POR} Beat Counter Abstraction: Parameterized Model Checking
               of Threshold-Based Distributed Algorithms},
  url       = {https://doi.org/10.1007/978-3-319-21690-4_6},
  volume    = {9206},
  year      = {2015}
}

@article{fmsdKonnovLVW17,
  author    = {Igor Konnov and
               Marijana Lazic and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/fmsd/KonnovLVW17.bib},
  doi       = {10.1007/S10703-017-0297-4},
  journal   = {Formal Methods Syst. Des.},
  number    = {2},
  pages     = {270--307},
  timestamp = {Fri, 13 Mar 2020 10:55:24 +0100},
  title     = {Para\({}^{\mbox{2}}\): parameterized path reduction, acceleration,
               and {SMT} for reachability in threshold-guarded distributed algorithms},
  url       = {https://doi.org/10.1007/s10703-017-0297-4},
  volume    = {51},
  year      = {2017}
}

@article{KonnovLVW16,
  author     = {Igor Konnov and
                Marijana Lazic and
                Helmut Veith and
                Josef Widder},
  bibsource  = {dblp computer science bibliography, https://dblp.org},
  biburl     = {https://dblp.org/rec/journals/corr/KonnovLVW16.bib},
  eprint     = {1608.05327},
  eprinttype = {arXiv},
  journal    = {CoRR},
  timestamp  = {Sat, 23 Jan 2021 01:20:12 +0100},
  title      = {A Short Counterexample Property for Safety and Liveness Verification
                of Fault-tolerant Distributed Algorithms},
  url        = {http://arxiv.org/abs/1608.05327},
  volume     = {abs/1608.05327},
  year       = {2016}
}

@inproceedings{KonnovLVW17,
  author    = {Igor V. Konnov and
               Marijana Lazic and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/popl/KonnovLVW17.bib},
  booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
               Programming Languages, {POPL} 2017, Paris, France, January 18-20,
               2017},
  doi       = {10.1145/3009837.3009860},
  editor    = {Giuseppe Castagna and
               Andrew D. Gordon},
  pages     = {719--734},
  publisher = {{ACM}},
  timestamp = {Sun, 19 Jan 2025 13:36:33 +0100},
  title     = {A short counterexample property for safety and liveness verification
               of fault-tolerant distributed algorithms},
  url       = {https://doi.org/10.1145/3009837.3009860},
  year      = {2017}
}


@inproceedings{0001W18,
  author    = {Igor Konnov and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/isola/0001W18.bib},
  booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.
               Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol,
               Cyprus, November 5-9, 2018, Proceedings, Part {III}},
  doi       = {10.1007/978-3-030-03424-5_22},
  editor    = {Tiziana Margaria and
               Bernhard Steffen},
  pages     = {327--342},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Sat, 05 Sep 2020 17:55:57 +0200},
  title     = {ByMC: Byzantine Model Checker},
  url       = {https://doi.org/10.1007/978-3-030-03424-5_22},
  volume    = {11246},
  year      = {2018}
}

@inproceedings{BertrandKLW19,
  author    = {Nathalie Bertrand and
               Igor Konnov and
               Marijana Lazic and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/concur/BertrandKLW19.bib},
  booktitle = {30th International Conference on Concurrency Theory, {CONCUR} 2019,
               Amsterdam, The Netherlands, August 27-30, 2019},
  doi       = {10.4230/LIPICS.CONCUR.2019.33},
  editor    = {Wan J. Fokkink and
               Rob van Glabbeek},
  pages     = {33:1--33:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  series    = {LIPIcs},
  timestamp = {Fri, 21 Nov 2025 14:06:54 +0100},
  title     = {Verification of Randomized Consensus Algorithms Under Round-Rigid
               Adversaries},
  url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.33},
  volume    = {140},
  year      = {2019}
}

@article{abs-2011-14789,
  author     = {Igor Konnov and
                Marijana Lazic and
                Ilina Stoilkovska and
                Josef Widder},
  bibsource  = {dblp computer science bibliography, https://dblp.org},
  biburl     = {https://dblp.org/rec/journals/corr/abs-2011-14789.bib},
  eprint     = {2011.14789},
  eprinttype = {arXiv},
  journal    = {CoRR},
  timestamp  = {Tue, 01 Dec 2020 14:59:59 +0100},
  title      = {Survey on Parameterized Verification with Threshold Automata and the
                Byzantine Model Checker},
  url        = {https://arxiv.org/abs/2011.14789},
  volume     = {abs/2011.14789},
  year       = {2020}
}

@article{0001LSW23,
  author    = {Igor Konnov and
               Marijana Lazic and
               Ilina Stoilkovska and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/lmcs/0001LSW23.bib},
  doi       = {10.46298/LMCS-19(1:5)2023},
  journal   = {Log. Methods Comput. Sci.},
  number    = {1},
  timestamp = {Sat, 30 Sep 2023 10:20:49 +0200},
  title     = {Survey on Parameterized Verification with Threshold Automata and the
               Byzantine Model Checker},
  url       = {https://doi.org/10.46298/lmcs-19(1:5)2023},
  volume    = {19},
  year      = {2023}
}

@misc{bymcgithub,
  author       = {Igor Konnov},
  howpublished = {\url{https://github.com/konnov/bymc/tree/266366f738bce9dbd5d04336fd9123d85ae2bca1}},
  note         = {[Online (GitHub); accessed 7-January-2026]},
  title        = {{ByMC - GitHub repository}},
  year         = {2012-2023}
}

@misc{bymcimggithub,
  author       = {Paul Eichler},
  howpublished = {\url{https://github.com/pleich/bymc/blob/0bca349cc7d3e8511f649726be4ce990f458c00a/bymc/Dockerfile}},
  note         = {[Online (GitHub); accessed 7-January-2026]},
  title        = {{ByMC - GitHub repository}},
  year         = {2025}
}

@misc{bymcvmgdrive,
  author       = {Igor Konnov},
  howpublished = {\url{https://drive.google.com/file/d/1m1LNeCPbEdOE35KBsVSsICeXQi8FM8gq/view?usp=share_link}},
  note         = {[Online (Google Drive); accessed 7-January-2026; link taken from the ByMC repository]},
  title        = {{ByMC Virtual Machine Image}},
  year         = {unknown}
}

@misc{benchmarksgithub,
  author       = {Igor Konnov},
  howpublished = {\url{https://github.com/konnov/fault-tolerant-benchmarks/tree/c9e8de463e0a6bc378d8f05270ffc7db043e79e6}},
  note         = {[Online (GitHub); accessed 7-January-2026]},
  title        = {{fault-tolerant-benchmarks - GitHub repository}},
  year         = {2014-2020}
}

@misc{synctagithub,
  author       = {Ilina Stoilkovska},
  howpublished = {\url{https://github.com/istoilkovska/syncTA/tree/9224ef50d5ada4782d0a1d5723531ebe43149584}},
  note         = {[Online (GitHub); accessed 7-January-2026]},
  title        = {{syncTA - GitHub repository}},
  year         = {2018-2021}
}

@misc{tacogithub,
  author       = {The TACO authors},
  howpublished = {PLACEHOLDER},
  note         = {[Online (GitHub); accessed 7-January-2026]},
  title        = {{TACO - GitHub repository}},
  year         = {2026}
}

@misc{tacoartifact,
  author       = {The TACO authors},
  howpublished = {PLACEHOLDER},
  note         = {[Online (Zenodo); accessed 7-January-2026]},
  title        = {{TACO - Artifact Package}},
  year         = {2026}
}

@inproceedings{SPIN13,
  author    = {Annu John and
               Igor Konnov and
               Ulrich Schmid and
               Helmut Veith and
               Josef Widder},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/spin/JohnKSVW13.bib},
  booktitle = {Model Checking Software - 20th International Symposium, {SPIN} 2013,
               Stony Brook, NY, USA, July 8-9, 2013. Proceedings},
  doi       = {10.1007/978-3-642-39176-7_14},
  editor    = {Ezio Bartocci and
               C. R. Ramakrishnan},
  pages     = {209--226},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Mon, 03 Apr 2023 17:23:33 +0200},
  title     = {Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms},
  url       = {https://doi.org/10.1007/978-3-642-39176-7_14},
  volume    = {7976},
  year      = {2013}
}

@inproceedings{StoilkovskaKWZ19,
  author    = {Ilina Stoilkovska and
               Igor Konnov and
               Josef Widder and
               Florian Zuleger},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/tacas/StoilkovskaKWZ19.bib},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 25th International Conference, {TACAS} 2019, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part
               {II}},
  doi       = {10.1007/978-3-030-17465-1_20},
  editor    = {Tom{\'{a}}s Vojnar and
               Lijun Zhang},
  pages     = {357--374},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  timestamp = {Sat, 05 Sep 2020 18:01:53 +0200},
  title     = {Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded
               Model Checking},
  url       = {https://doi.org/10.1007/978-3-030-17465-1_20},
  volume    = {11428},
  year      = {2019}
}

@article{StoilkovskaKWZ22,
  author    = {Ilina Stoilkovska and
               Igor Konnov and
               Josef Widder and
               Florian Zuleger},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/sttt/StoilkovskaKWZ22.bib},
  doi       = {10.1007/S10009-021-00637-9},
  journal   = {Int. J. Softw. Tools Technol. Transf.},
  number    = {1},
  pages     = {33--48},
  timestamp = {Sat, 30 Sep 2023 10:27:14 +0200},
  title     = {Verifying safety of synchronous fault-tolerant algorithms by bounded
               model checking},
  url       = {https://doi.org/10.1007/s10009-021-00637-9},
  volume    = {24},
  year      = {2022}
}

@inproceedings{KonnovWSS17,
  author       = {Igor V. Konnov and
                  Josef Widder and
                  Francesco Spegni and
                  Luca Spalazzi},
  editor       = {Ahmed Bouajjani and
                  David Monniaux},
  title        = {Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed
                  Algorithms},
  booktitle    = {Verification, Model Checking, and Abstract Interpretation - 18th International
                  Conference, {VMCAI} 2017, Paris, France, January 15-17, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10145},
  pages        = {347--366},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-52234-0_19},
  doi          = {10.1007/978-3-319-52234-0_19},
  timestamp    = {Sat, 09 Apr 2022 12:46:16 +0200},
  biburl       = {https://dblp.org/rec/conf/vmcai/KonnovWSS17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}