Verifying Safety Properties With the TLA+ Proof System

Kaustuv Chaudhuri 1, * Damien Doligez 2 Leslie Lamport 3 Stephan Merz 4
* Auteur correspondant
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties.
Type de document :
Communication dans un congrès
Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.142--148, 2010, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-14203-1_12〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00534821
Contributeur : Kaustuv Chaudhuri <>
Soumis le : mercredi 10 novembre 2010 - 15:45:59
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : vendredi 11 février 2011 - 03:13:43

Fichiers

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

Identifiants

Citation

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. Verifying Safety Properties With the TLA+ Proof System. Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.142--148, 2010, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-14203-1_12〉. 〈inria-00534821〉

Partager

Métriques

Consultations de la notice

438

Téléchargements de fichiers

429