Harnessing SMT Solvers for TLA+ Proofs

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.
Type de document :
Communication dans un congrès
Gerald Lüttgen and Stephan Merz. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. EASST, 53, 2012, ECEASST
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00760579
Contributeur : Stephan Merz <>
Soumis le : mardi 4 décembre 2012 - 10:01:13
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : samedi 17 décembre 2016 - 19:39:03

Fichiers

avocs2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00760579, version 1

Collections

Citation

Stephan Merz, Hernán Vanzetto. Harnessing SMT Solvers for TLA+ Proofs. Gerald Lüttgen and Stephan Merz. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. EASST, 53, 2012, ECEASST. 〈hal-00760579〉

Partager

Métriques

Consultations de la notice

327

Téléchargements de fichiers

390