Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Tuesday, September 28, 2010 - 6:24:24 PM
Last modification on : Friday, January 21, 2022 - 3:15:22 AM

Links full text




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⟩



Les métriques sont temporairement indisponibles