Symbolic model checking for TLA+ made faster
From MaRDI portal
Publication:6535348
DOI10.1007/978-3-031-30823-9_7zbMATH Open1543.68227MaRDI QIDQ6535348FDOQ6535348
Authors: Rodrigo Otoni, Jure Kukovec, Patrick Eugster, Natasha Sharygina 
Publication date: 13 December 2023
Recommendations
- Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
- Formal verification of Multi-Paxos for distributed consensus
- Distributed symbolic model checking for \(\mu\)-calculus
- scientific article; zbMATH DE number 1798187
- Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Asynchronous consensus and broadcast protocols
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- On the hardness of failure-sensitive agreement problems.
- Verification of threshold-based distributed algorithms by decomposition to decidable logics
- Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
This page was built for publication: Symbolic model checking for TLA+ made faster
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535348)
