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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00521886
Contributor : Stephan Merz <>
Submitted on : Tuesday, September 28, 2010 - 6:24:24 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM

Links full text

Identifiers

Collections

Citation

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. The TLA+ Proof System: Building a Heterogeneous Verification Platform. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩. ⟨inria-00521886⟩

Share

Metrics

Record views

422