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
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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
Liste complète des métadonnées

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00760579
Contributor : Stephan Merz <>
Submitted on : Tuesday, December 4, 2012 - 10:01:13 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Document(s) archivé(s) le : Saturday, December 17, 2016 - 7:39:03 PM

Files

avocs2012.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00760579, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

380

Files downloads

505