Skip to Main content Skip to Navigation
Conference papers

Towards certification 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 Zermelo-Fränkel 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. We introduce a typing discipline for TLA+ proof obligations, which helps us to disambiguate the translation of expressions of (untyped) TLA+, while ensuring its soundness. Our work is a first step towards the certification of proofs generated by proof-producing SMT solvers in Isabelle/TLA+, which is intended to be the only trusted component of TLAPS.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, November 28, 2011 - 10:27:56 AM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM
Long-term archiving on: : Monday, December 5, 2016 - 8:26:58 AM


Files produced by the author(s)


  • HAL Id : hal-00645458, version 1



Stephan Merz, Hernán Vanzetto. Towards certification of TLA+ proof obligations with SMT solvers. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland. ⟨hal-00645458⟩



Les métriques sont temporairement indisponibles