Automatic Verification Of TLA+ Proof Obligations With SMT Solvers

Stephan Merz 1, 2 Hernán Vanzetto 1, 2
1 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
Abstract : TLA+ is a formal specification language that is based on ZF set theory and the Temporal Logic of Actions TLA. The TLA+ proof system TLAPS assists users in deductively verifying safety properties of TLA+ specifications. TLAPS is built around a proof manager, which interprets the TLA+ proof language, generates corresponding proof obligations, and passes them to backend verifiers. In this paper we present a new backend for use with SMT solvers that supports elementary set theory, functions, arithmetic, tuples, and records. Type information required by the solvers is provided by a typing discipline for TLA+ proof obligations, which helps us disambiguate the translation of expressions of (untyped) TLA+, while ensuring its soundness. Preliminary results show that the backend can help to significantly increase the degree of automation of certain interactive proofs.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-00760570
Contributor : Stephan Merz <>
Submitted on : Tuesday, December 4, 2012 - 9:51:59 AM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Long-term archiving on : Saturday, December 17, 2016 - 7:30:19 PM

Files

tla2smt.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Stephan Merz, Hernán Vanzetto. Automatic Verification Of TLA+ Proof Obligations With SMT Solvers. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. pp.289-303, ⟨10.1007/978-3-642-28717-6_23⟩. ⟨hal-00760570⟩

Share

Metrics

Record views

370

Files downloads

523