pith. machine review for the scientific record. sign in

arxiv: 2605.06118 · v1 · submitted 2026-05-07 · 💻 cs.DC

Recognition: unknown

TACO: A Toolsuite for the Verification of Threshold Automata

Paul Eichler , Tom Baumeister , Mouhammad Sakr , Mahboubeh Kalateh Dowlati , Marcus V\"olp , Swen Jacobs
Authors on Pith no claims yet

Pith reviewed 2026-05-08 05:12 UTC · model grok-4.3

classification 💻 cs.DC
keywords threshold automatamodel checkingdistributed algorithmsfault toleranceverification toolsuitesemi-decision procedures
0
0 comments X

The pith

TACO implements three model checking approaches for threshold automata in decidable fragments plus two semi-decision procedures for verifying fault-tolerant distributed algorithms.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents TACO as a modular and extensible toolsuite for developing and automatically verifying threshold-based distributed algorithms. It equips the suite with three established model checking methods that cover different decidable fragments of threshold automata and adds two semi-decision procedures that handle cases outside those fragments. A reader would care because the work turns theoretical decidability results into practical, documented tools that can check correctness properties of algorithms designed to tolerate faults.

Core claim

TACO implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments, while providing a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata.

What carries the argument

The TACO toolsuite, which integrates model checking algorithms for threshold automata and supports extension with new methods.

If this is right

  • Developers can apply the three decidable model checkers to verify properties of threshold automata arising in fault-tolerant algorithms.
  • The semi-decision procedures extend verification coverage to automata outside the known decidable fragments.
  • The modular architecture lets users add new verification algorithms without rebuilding the entire suite.
  • Experimental runs demonstrate the practical performance of the implemented methods on representative examples.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The toolsuite could reduce manual proof effort when engineers design new threshold-based protocols by offering automated checks during development.
  • Integration with existing distributed-systems simulators might allow end-to-end testing that combines model checking with concrete execution traces.
  • Further extensions of the semi-decision procedures could target additional classes of liveness properties common in fault-tolerant settings.

Load-bearing premise

The three model checking approaches correctly realize the decidable fragments from the literature and the semi-decision procedures remain sound on the cases they address.

What would settle it

A concrete threshold automaton and property where TACO returns an incorrect verification outcome while independent analysis or another tool produces the opposite result.

Figures

Figures reproduced from arXiv: 2605.06118 by Mahboubeh Kalateh Dowlati, Marcus V\"olp, Mouhammad Sakr, Paul Eichler, Swen Jacobs, Tom Baumeister.

Figure 2
Figure 2. Figure 2: TA of the algorithm in view at source ↗
Figure 3
Figure 3. Figure 3: Architecture of the TACO toolsuite Tool-Supported Modelling Languages. Taco supports models in two differ￾ent languages. The first is an extension of the language introduced by ByMC for modelling threshold automata [22, 23, 29], which are usually denoted by the file ending .ta (.eta for extended threshold automata). The second is a fragment of TLA+ [34], a more well-known language for model checking, which… view at source ↗
Figure 4
Figure 4. Figure 4: Pseudocode of a reliable broadcast protocol. V0 V1 RV0 SE AC rec++ nsnt++; rec++ nsnt ≥ φ1 nsnt ≥ φ2 rec ≥ φ3 ∧ nsnt < φ2 nsnt := 0; rec := 0 rec = 0 rec ≥ φ3 ∧ nsnt < φ1 nsnt := 0; rec := 0 rec = 0 φ1 = t − f + 1 φ2 = n − t − f φ3 = n − f view at source ↗
Figure 6
Figure 6. Figure 6: Screenshot of the counterexample reported ByMC in the view at source ↗
read the original abstract

We present TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. Our toolsuite implements three approaches for model checking threshold automata in different decidable fragments known from the literature and two semi-decision procedures going beyond these decidable fragments. Moreover, TACO is a modular, extensible, and well-documented framework for developing algorithms and tools for threshold automata. We present important features, give an overview of the implemented algorithms, and evaluate their performance experimentally.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents TACO, a toolsuite for the development and automatic verification of fault-tolerant and threshold-based distributed algorithms. It implements three model-checking approaches for threshold automata in different decidable fragments from the literature, plus two semi-decision procedures that extend beyond those fragments. The manuscript also describes a modular, extensible framework for developing algorithms and tools for threshold automata, provides an overview of the implemented algorithms, and reports experimental performance results.

Significance. If the implementations faithfully realize the cited approaches, TACO would supply a practical, extensible platform for verifying threshold automata models of distributed algorithms. This addresses a recurring need in formal methods for distributed systems by combining established decidable fragments with semi-decision procedures and by offering a documented framework that can be extended by other researchers. The experimental evaluation, if reproducible, would further demonstrate the tool's utility on realistic benchmarks.

major comments (1)
  1. §4 (overview of implemented algorithms): the description of the two semi-decision procedures states that they 'go beyond' the decidable fragments but supplies only high-level pseudocode without an explicit soundness argument or reference to a machine-checked proof for the specific implementation choices; because soundness of these procedures is load-bearing for the central claim that TACO correctly handles cases outside the decidable fragments, a self-contained argument or pointer to a verified reference implementation is required.
minor comments (2)
  1. The experimental section should include the exact benchmark suite (e.g., file names or repository commit) and the hardware configuration used for the reported runtimes so that the performance claims can be reproduced.
  2. Notation for threshold automata (e.g., the definition of guards and the semantics of 'threshold' predicates) is introduced only informally in the introduction; a compact formal definition in a dedicated preliminary section would improve readability for readers unfamiliar with the cited literature.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation and the recommendation for minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [—] §4 (overview of implemented algorithms): the description of the two semi-decision procedures states that they 'go beyond' the decidable fragments but supplies only high-level pseudocode without an explicit soundness argument or reference to a machine-checked proof for the specific implementation choices; because soundness of these procedures is load-bearing for the central claim that TACO correctly handles cases outside the decidable fragments, a self-contained argument or pointer to a verified reference implementation is required.

    Authors: We agree that the soundness of the semi-decision procedures is central and that the current high-level pseudocode in §4 does not supply an explicit argument for the implementation choices. The two procedures are direct adaptations of algorithms whose soundness is established in the cited literature on threshold automata (specifically, the extensions beyond the decidable fragments described in the foundational papers). To address the referee's concern, we will revise §4 in the next version to include a concise, self-contained soundness sketch that explains how the concrete implementation choices preserve the key invariants and termination properties from those references. We do not claim a machine-checked proof of the TACO code itself; instead, the revision will make the reduction to the proven cases explicit. This change will be limited to added explanatory text and does not alter the tool's behavior or experimental results. revision: yes

Circularity Check

0 steps flagged

No significant circularity; implementation of cited algorithms

full rationale

The manuscript describes a modular toolsuite that implements three model-checking procedures for known decidable fragments of threshold automata plus two sound semi-decision procedures. No mathematical derivation chain, equations, fitted parameters, or predictions are present. Claims rest on faithful implementation of externally cited fragments and experimental performance data rather than any self-referential reduction or load-bearing self-citation. The structure is self-contained as a software-engineering contribution with no internal circularity.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is a description of a software toolsuite and does not introduce or rely on new free parameters, mathematical axioms, or invented entities beyond standard model-checking theory.

pith-pipeline@v0.9.0 · 5394 in / 1016 out tokens · 31324 ms · 2026-05-08T05:12:48.998164+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

51 extracted references · 31 canonical work pages

  1. [1]

    In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996

    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 313–321. IEEE Computer Society (1996).https://doi.org/10.1109/LICS.1996. 561359

    work page doi:10.1109/lics.1996 1996

  2. [2]

    Balasubramanian, A.R.: Source Code: Complexity of Verification and Synthesis of Threshold Automata, A. R. Balasubramanian, J. Esparza, M. Lazic; ATVA20. https://github.com/arbalan96/thr_aut_SMT(2025), [Online (GitHub); accessed 22-April-2026]

    2025

  3. [3]

    In: Hung, D.V., Sokolsky, O

    Balasubramanian, A.R., Esparza, J., Lazic, M.: Complexity of verification and synthesis of threshold automata. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Com- puter Science, vol. 12302, pp. 144–160. Spri...

    2020

  4. [4]

    In: Fisman, D., Rosu, G

    Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems -...

    work page doi:10.1007/978-3-030-99524-9_24 2022

  5. [5]

    In: Proceedings of the 8th International Workshop on Satisfiability Modulo The- ories (Edinburgh, UK)

    Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo The- ories (Edinburgh, UK). vol. 13, p. 14 (2010),https://smt-lib.org/papers/ smt-lib-reference-v2.0-r10.12.21.pdf

    2010

  6. [6]

    In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M

    Baumeister, T., Eichler, P., Jacobs, S., Sakr, M., Völp, M.: Parameterized verifi- cation of round-based distributed algorithms via extended threshold automata. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceed- ings, Part I. Lecture Notes in Co...

    work page doi:10.1007/978-3-031-71162-6_33 2024

  7. [7]

    424–426 (2022)

    Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Brief announcement: Holistic verification of blockchain consensus pp. 424–426 (2022). https://doi.org/10.1145/3519270.3538468

    work page doi:10.1145/3519270.3538468 2022

  8. [8]

    In: Fokkink, W.J., van Glabbeek, R

    Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consen- sus algorithms under round-rigid adversaries. In: Fokkink, W.J., van Glabbeek, R. TACO: A Toolsuite for the Verification of Threshold Automata 13 (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, Am- sterdam, The Netherlands, August 27-30, 2019. LIPI...

    2019

  9. [9]

    Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824–840 (1985).https://doi.org/10.1145/4221.214134

    work page doi:10.1145/4221.214134 1985

  10. [10]

    In: Malyshkin, V.E

    Brasileiro, F.V., Greve, F., Mostéfaoui, A., Raynal, M.: Consensus in one com- munication step. In: Malyshkin, V.E. (ed.) Parallel Computing Technologies, 6th International Conference, PaCT 2001, Novosibirsk, Russia, September 3-7, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2127, pp. 42–50. Springer (2001).https://doi.org/10.1007/3-540-44743-1_4

    work page doi:10.1007/3-540-44743-1_4 2001

  11. [11]

    In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021

    Crain, T., Natoli, C., Gramoli, V.: Red belly: A secure, fair and scalable open blockchain. In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. pp. 466–483. IEEE (2021).https://doi. org/10.1109/SP40001.2021.00087

    work page doi:10.1109/sp40001.2021.00087 2021

  12. [12]

    Eichler, P., Baumeister, T., Sakr, M., Dowlati, M.K., Völp, M., Jacobs, S.: TACO - Artifact Package.https://doi.org/10.5281/zenodo.19659446(2026), [Online (Zenodo); accessed 22-April-2026]

    work page doi:10.5281/zenodo.19659446(2026 2026

  13. [13]

    In: Krishna, S., Sankaranarayanan, S., Trivedi, A

    Eichler, P., Jacobs, S., Weil-Kennedy, C.: Parameterized verification of systems with precise (0,1)-counter abstraction. In: Krishna, S., Sankaranarayanan, S., Trivedi, A. (eds.) Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part I. Lecture Notes in...

    work page doi:10.1007/978-3-031-82700-6_5 2025

  14. [14]

    In: Ottmann, T

    Finkel, A.: A generalization of the procedure of karp and miller to well structured transition systems. In: Ottmann, T. (ed.) Automata, Languages and Programming, 14th International Colloquium, ICALP87, Karlsruhe, Germany, July 13-17, 1987, Proceedings. Lecture Notes in Computer Science, vol. 267, pp. 499–508. Springer (1987).https://doi.org/10.1007/3-540...

    work page doi:10.1007/3-540-18088-5_43 1987

  15. [15]

    Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems.Commun.ACM60(7),83–92(2017).https://doi.org/10.1145/3068608

    work page doi:10.1145/3068608 2017

  16. [16]

    Husung, N., Dubslaff, C., Hermanns, H., Köhl, M.A.: OxiDD: A safe, concurrent, modular, and performant decision diagram framework in Rust. In: Proceedings of the 30th International Conference on Tools and Algorithms for the Construc- tion and Analysis of Systems (TACAS’24) (2024).https://doi.org/10.1007/ 978-3-031-57256-2_13

    2024

  17. [17]

    Jaber, N., Wagner, C., Jacobs, S., Kulkarni, M., Samanta, R.: Quicksilver: mod- eling and parameterized verification for distributed agreement-based systems. Proc. ACM Program. Lang.5(OOPSLA), 1–31 (2021).https://doi.org/10. 1145/3485534

    2021

  18. [18]

    In: Formal Meth- ods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23,

    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Formal Meth- ods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23,

    2013

  19. [19]

    pp. 201–209. IEEE (2013).https://doi.org/10.1109/FMCAD.2013.6679411

    work page doi:10.1109/fmcad.2013.6679411 2013

  20. [20]

    In: Bartocci, E., Ramakrish- nan, C.R

    John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrish- nan, C.R. (eds.) Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings. Lecture Notes in Com- puter Science, vol. 7976, pp. 209–226. ...

    2013

  21. [21]

    IEEE Trans

    Jr., S.B.A.: Binary decision diagrams. IEEE Trans. Computers27(6), 509–516 (1978).https://doi.org/10.1109/TC.1978.1675141

    work page doi:10.1109/tc.1978.1675141 1978

  22. [22]

    Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Int. J. Softw. Tools Technol. Transf.2(4), 328–342 (2000). https://doi.org/10.1007/S100090050040

    work page doi:10.1007/s100090050040 2000

  23. [23]

    Konnov, I.: ByMC - GitHub repository.https://github.com/konnov/bymc/tree/ 266366f738bce9dbd5d04336fd9123d85ae2bca1(2012-2023), [Online (GitHub); ac- cessed 7-January-2026]

    2012

  24. [24]

    https://github.com/konnov/fault-tolerant-benchmarks/tree/ c9e8de463e0a6bc378d8f05270ffc7db043e79e6(2014-2020), [Online (GitHub); accessed 7-January-2026]

    Konnov, I.: fault-tolerant-benchmarks - GitHub repository. https://github.com/konnov/fault-tolerant-benchmarks/tree/ c9e8de463e0a6bc378d8f05270ffc7db043e79e6(2014-2020), [Online (GitHub); accessed 7-January-2026]

    2014

  25. [25]

    Konnov, I., Lazic, M., Stoilkovska, I., Widder, J.: Survey on parameterized verifi- cation with threshold automata and the byzantine model checker. Log. Methods Comput. Sci.19(1) (2023).https://doi.org/10.46298/LMCS-19(1:5)2023

    work page doi:10.46298/lmcs-19(1:5)2023 2023

  26. [26]

    CoRR abs/1608.05327(2016).https://doi.org/10.1145/3009837.3009860

    Konnov, I., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. CoRR abs/1608.05327(2016).https://doi.org/10.1145/3009837.3009860

    work page doi:10.1145/3009837.3009860 2016

  27. [27]

    Formal Methods Syst

    Konnov, I., Lazic, M., Veith, H., Widder, J.: Para2: parameterized path reduc- tion, acceleration, and SMT for reachability in threshold-guarded distributed algo- rithms. Formal Methods Syst. Des.51(2), 270–307 (2017).https://doi.org/10. 1007/S10703-017-0297-4

    2017

  28. [28]

    In: Baldan, P., Gorla, D

    Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8704, pp. 125–140. ...

    2014

  29. [29]

    In: Kroen- ing, D., Pasareanu, C.S

    Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: Pa- rameterized model checking of threshold-based distributed algorithms. In: Kroen- ing, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science...

    work page doi:10.1007/978-3-319-21690-4_6 2015

  30. [30]

    In: Margaria, T., Steffen, B

    Konnov, I., Widder, J.: Bymc: Byzantine model checker. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Valida- tion. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11246, pp. 327–342. Springe...

    2018

  31. [31]

    In: Castagna, G., Gordon, A.D

    Konnov, I.V., Lazic, M., Veith, H., Widder, J.: A short counterexample prop- erty for safety and liveness verification of fault-tolerant distributed algorithms. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Sym- posium on Principles of Programming Languages, POPL 2017, Paris, France, Jan- uary 18-20, 2017. pp. 719–734. ACM (201...

    work page doi:10.1145/3009837 2017

  32. [32]

    In: Mazzara, M., Voronkov, A

    Konnov, I.V., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Mazzara, M., Voronkov, A. (eds.) Perspectives of System Informatics - 10th International Andrei Ershov In- formatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopo- TACO: A Toolsuite for the Verification...

    2015

  33. [33]

    Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model check- ing for threshold-based distributed algorithms: Reachability. Inf. Comput.252, 95–109 (2017).https://doi.org/10.1016/J.IC.2016.03.006

    work page doi:10.1016/j.ic.2016.03.006 2017

  34. [34]

    In: Schewe, S., Zhang, L

    Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: All flavors of threshold automata. In: Schewe, S., Zhang, L. (eds.) 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. LIPIcs, vol. 118, pp. 19:1–19:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018).https://doi.org/10....

    work page doi:10.4230/lipics.concur.2018.19 2018

  35. [35]

    Addison-Wesley (2002),http://research.microsoft

    Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002),http://research.microsoft. com/users/lamport/tla/book.html

    2002

  36. [36]

    ACM Trans

    Lamport, L., Shostak, R.E., Pease, M.C.: The byzantine generals problem. ACM Trans. Program. Lang. Syst.4(3), 382–401 (1982).https://doi.org/10.1145/ 357172.357176

    work page arXiv 1982

  37. [37]

    McMillan and Oded Padon

    McMillan, K.L., Padon, O.: Ivy: A multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 190–202. Springer (2020).https://doi.org/10.100...

    work page doi:10.1007/978-3-030-53291-8_12 2020

  38. [38]

    In: 2003 International Conference on De- pendable Systems and Networks (DSN 2003), 22-25 June 2003, San Francisco, CA, USA, Proceedings

    Mostéfaoui,A.,Mourgaya,E.,Parvédy,P.R.,Raynal,M.:Evaluatingthecondition- based approach to solve consensus. In: 2003 International Conference on De- pendable Systems and Networks (DSN 2003), 22-25 June 2003, San Francisco, CA, USA, Proceedings. pp. 541–550. IEEE Computer Society (2003).https: //doi.org/10.1109/DSN.2003.1209964

    work page doi:10.1109/dsn.2003.1209964 2003

  39. [39]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) 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. Proceedi...

    2008

  40. [40]

    In: Piskac, R., Rakamaric, Z

    Pîrlea, G., Gladshtein, V., Kinsbruner, E., Zhao, Q., Sergey, I.: Veil: A framework for automated and interactive verification of transition systems. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III. Lecture Notes in Computer Science, vol. 1...

    work page doi:10.1007/978-3-031-98682-6_2 2025

  41. [41]

    In: Brinksma, E., Larsen, K.G

    Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th Interna- tional Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceed- ings. Lecture Notes in Computer Science, vol. 2404, pp. 107–122. Springer (2002). https://doi.org/10.1007/3-540-45657-0_9

    work page doi:10.1007/3-540-45657-0_9 2002

  42. [42]

    Electron

    Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, ver- ification, and implementation of fault-tolerant systems using eventml. Electron. Commun.Eur.Assoc.Softw.Sci.Technol.72(2015).https://doi.org/10.14279/ TUJ.ECEASST.72.1013 16 P. Eichler, T. Baumeister, M. Sakr, M. K. Dowlati, M. Völp and S. Jacobs

    2015

  43. [43]

    Public Software, University of Colorado (1997), online (GitHub Mirror); accessed 16-January-2026;https:// github.com/cuddorg/cudd/tree/f54f533303640afd5dbe47a05ebeabb3066f2a25

    Somenzi, F.: Cudd: Cu decision diagram package. Public Software, University of Colorado (1997), online (GitHub Mirror); accessed 16-January-2026;https:// github.com/cuddorg/cudd/tree/f54f533303640afd5dbe47a05ebeabb3066f2a25

    1997

  44. [44]

    Somenzi, F.: Efficient manipulation of decision diagrams. Int. J. Softw. Tools Tech- nol. Transf.3(2), 171–181 (2001).https://doi.org/10.1007/S100090100042

    work page doi:10.1007/s100090100042 2001

  45. [45]

    Distributed Comput.2(2), 80–94 (1987).https://doi

    Srikanth, T.K., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Comput.2(2), 80–94 (1987).https://doi. org/10.1007/BF01667080

    work page doi:10.1007/bf01667080 1987

  46. [46]

    In: Vojnar, T., Zhang, L

    Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In: Vojnar, T., Zhang, L. (eds.) 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 S...

    2019

  47. [47]

    In: Hung, D.V., Sokolsky, O

    Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Eliminating message counters in threshold automata. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technol- ogy for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 196–212. Springer ...

    2020

  48. [48]

    In: Henglein, F., Shoham, S., Vizel, Y

    Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Eliminating message counters in synchronous threshold automata. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceed- ings. Lecture Notes in Computer Scienc...

    work page doi:10.1007/978-3-030-67067-2_10 2021

  49. [49]

    Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. Int. J. Softw. Tools Technol. Transf.24(1), 33–48 (2022).https://doi.org/10.1007/S10009-021-00637-9

    work page doi:10.1007/s10009-021-00637-9 2022

  50. [50]

    In: Sankaranarayanan, S., Sharygina, N

    Thomas, B., Sankur, O.: Pylta: A verification tool for parameterized distributed algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) 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, Fran...

    work page doi:10.1007/978-3-031-30820-8_4 2023

  51. [51]

    V0", "V1

    Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Im- plementation, Portland, OR, USA, June 15-17, 2015. pp. 357–368...

    work page doi:10.1145/2737924.2737958 2015