Towards certification of TLA+ proof obligations with SMT solvers - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Towards certification of TLA+ proof obligations with SMT solvers

(1, 2) , (1, 2)
1
2

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.
Fichier principal
Vignette du fichier
tla2smt.pdf (218.82 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00645458 , version 1 (28-11-2011)

Identifiers

  • HAL Id : hal-00645458 , version 1

Cite

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⟩
196 View
235 Download

Share

Gmail Facebook Twitter LinkedIn More