The TLA+ Proof System: Building a Heterogeneous Verification Platform

Kaustuv Chaudhuri 1 Damien Doligez 2, 3 Leslie Lamport 3, 4 Stephan Merz 3, 5
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
5 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs. Proofs are written in TLA+, which contains a hierarchical proof language based on elementary mathematics. It has been designed independently of any specific verification tool or strategy. TLAPS consists of a front-end, called the proof manager, and of a collection of back-end verifiers that include theorem provers, SMT solvers, and decision procedures. The proof manager interprets TLA+ proofs and generates the corresponding proof obligations that must be verified. The current release handles almost all the non-temporal part of TLA+, which suffices for proving standard safety properties, but not liveness properties. The proof manager supports hierarchical and non-linear proof construction and verification so that the skeleton of an incomplete proof can be verified independently of the lower-level subproofs.
Type de document :
Communication dans un congrès
Ana Cavalcanti and David Déharbe and Marie-Claude Gaudel and Jim Woodcock. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. Springer, 6255, pp.44, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14808-8_3〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00521886
Contributeur : Stephan Merz <>
Soumis le : mardi 28 septembre 2010 - 18:24:24
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01

Identifiants

Citation

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. The TLA+ Proof System: Building a Heterogeneous Verification Platform. Ana Cavalcanti and David Déharbe and Marie-Claude Gaudel and Jim Woodcock. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. Springer, 6255, pp.44, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14808-8_3〉. 〈inria-00521886〉

Partager

Métriques

Consultations de la notice

379