Symbolic model checking for TLA+ made faster

DOI10.1007/978-3-031-30823-9_7MaRDI QIDQ6535348zbMATH OpenFDO

Authors Rodrigo Otoni, Jure Kukovec, Patrick Eugster, Natasha Sharygina

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30823-9_7

zbMATH Keywords

distributed algorithmsmodel checkingSMT arrays

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed algorithms (68W15)

Recommendations

• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Formal verification of Multi-Paxos for distributed consensus
• Distributed symbolic model checking for -calculus
• scientific article; zbMATH DE number 1798187
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications

Cites work

• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Asynchronous consensus and broadcast protocols
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
• On the hardness of failure-sensitive agreement problems.
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Verification of threshold-based distributed algorithms by decomposition to decidable logics

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)