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
2 MSR - INRIA - Microsoft Research - Inria Joint Centre

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.

Domaines: Logique en informatique [cs.LO]

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⟩