Automatic Verification of TLA + Proof Obligations with SMT Solvers

DOI10.1007/978-3-642-28717-6_23zbMath1352.68159OpenAlexW29617856MaRDI QIDQ2891459

Hernán Vanzetto, Stephan Merz

Publication date: 15 June 2012

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00760570/file/tla2smt.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

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

Uses Software

• Isabelle
• SMT-LIB
• Yices
• cvc3
• z3
• Zenon
• Sledgehammer
• TLAPS