A TLA+ Proof System - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

A TLA+ Proof System

Résumé

We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Different provers can be used to verify different obligations. The currently supported back-ends are the tableau prover Zenon and Isabelle/TLA+, an axiomatisation of TLA+ in Isabelle/Pure. The proof obligations for a complete TLA+ proof can also be used to certify the theorem in Isabelle/TLA+.
Fichier principal
Vignette du fichier
main.pdf (180.59 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00338299 , version 1 (12-11-2008)

Identifiants

  • HAL Id : inria-00338299 , version 1
  • ARXIV : 0811.1914

Citer

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. A TLA+ Proof System. Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar. ⟨inria-00338299⟩
282 Consultations
1283 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More