Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

Uses Software

• CPAchecker
• TLAPS
• TLC
• CBMC
• Cubicle
• GitHub

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