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 metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00645458
Contributor : Stephan Merz <>
Submitted on : Monday, November 28, 2011 - 10:27:56 AM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Long-term archiving on : Monday, December 5, 2016 - 8:26:58 AM

File

tla2smt.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00645458, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

398

Files downloads

295