Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Tuesday, December 4, 2012 - 9:51:59 AM
Last modification on : Friday, February 4, 2022 - 3:25:12 AM
Long-term archiving on: : Saturday, December 17, 2016 - 7:30:19 PM


Files produced by the author(s)




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⟩



Record views


Files downloads