Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
From MaRDI portal
Publication:5881447
DOI10.1007/978-3-319-91271-4_7OpenAlexW2800425952MaRDI QIDQ5881447
No author found.
Publication date: 10 March 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-91271-4_7
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Uses Software
Cites Work
- Unnamed Item
- On the hardness of failure-sensitive agreement problems.
- Logics of specification languages
- Automatic Verification of TLA + Proof Obligations with SMT Solvers
- Counterexample-guided abstraction refinement for symbolic model checking
- Asynchronous consensus and broadcast protocols
- Unreliable failure detectors for reliable distributed systems
- Disk Paxos
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms