Skip to Main content Skip to Navigation
New interface
Conference papers

Harnessing SMT Solvers for TLA+ Proofs

Stephan Merz 1, 2 Hernán Vanzetto 1, 2 
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : TLA+ is a language based on Zermelo-Fraenkel set theory and linear temporal logic designed for specifying and verifying concurrent and distributed algorithms and systems. The TLA+ proof system TLAPS allows users to interactively verify safety properties of these systems. At the core of TLAPS, a proof manager interprets the proof language, generates corresponding proof obligations and passes them to backend provers. We recently developed a backend that relies on a typing discipline to encode (untyped) TLA+ formulas into multi-sorted first-order logic for SMT solvers. In this paper we present a different encoding of TLA+ formulas that does not require explicit type inference for TLA+ expressions. We also present a number of techniques based on rewriting in order to simplify the resulting formulas.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Tuesday, December 4, 2012 - 10:01:13 AM
Last modification on : Friday, November 18, 2022 - 9:26:13 AM
Long-term archiving on: : Saturday, December 17, 2016 - 7:39:03 PM


Files produced by the author(s)


  • HAL Id : hal-00760579, version 1



Stephan Merz, Hernán Vanzetto. Harnessing SMT Solvers for TLA+ Proofs. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. ⟨hal-00760579⟩



Record views


Files downloads