Tools for Proofs

TLA+

Goals of the project

TLA+ is a specification and proof language based on temporal logic, where first-order logic and set theory are used to describe a set of states and the possible transitions between these states. TLA+ also includes a module system for manipulating large-scale specifications.

 There are a number of existing tools for working on TLA+ specifications, the most important of which is the TLC model-checker. Although the proof side of TLA+ is not well-developed yet, with no proof tools and an incomplete definition of the proof language, TLA+ has already proved its worth in significant projects in hardware design (Alpha and Itanium processors), protocols (PCI-X), and software (Doligez-Leroy-Gonthier garbage collector).

In this project, we are working on turning TLA+ into a complete solution for writing, debugging, and proving specifications. More precisely, we are concentrating on the proof aspect:

  • refining the proof language
  • making a development environment for TLA+ specifications and proofs
  • developing and adapting automatic tools for helping to prove TLA+ theorems (Zenon, veriT)
  • translating TLA+ proofs into a machine-checkable format for verification by an independent checker (Isabelle)

We will validate and enhance our tools by finding examples of real-world projects where formal specifications bring real improvements over other methodologies. Feedback from these examples will help us improve the proof language and the tools and develop methods and “design patterns” for using TLA+.

  • Doligez
    Damien Doligez
    Researcher, member of the Gallium team at INRIA Paris-Rocquencourt Author of the Zenon automatic theorem prover ...

2014

Communications avec actes

Titre
Refinement Types for TLA+
Auteurs
Stephan Merz url; Hernán Vanzetto
Détail
Julia M. Badger and Kristin Yvonne Rozier. NASA Formal Methods – 6th International Symposium, 2014, Houston, Texas, United States. Springer, 8430, pp. 143-157, LNCS
Accès au bibtex
BibTex

Communications sans actes

Titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Auteurs
Damien Doligez; Jael Kriener; Leslie Lamport; Tomer Libal; Stephan Merz url
Détail
ARQNL 2014 – Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria.
Accès au texte intégral et bibtex
final.pdf final.ps BibTex

2012

Communications avec actes

Titre
TLA+ Proofs
Auteurs
Denis Cousineau; Damien Doligez; Leslie Lamport; Stephan Merz url; Daniel Ricketts; Hernán Vanzetto
Détail
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods – FM 2012, Aug 2012, Paris, France. Springer, FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, 7436, pp. 147-154, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
final.pdf BibTex
Titre
Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
Auteurs
Stephan Merz url; Hernán Vanzetto
Détail
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela, Bolivarian Republic Of. Springer, Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2012), 7180, pp. 289-303, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
tla2smt.pdf BibTex
Titre
Harnessing SMT Solvers for TLA+ Proofs
Auteurs
Stephan Merz url; Hernán Vanzetto
Détail
Gerald Lüttgen and Stephan Merz. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. EASST, Automated Verification of Critical Systems (AVoCS 2012), 53, ECEASST
Accès au texte intégral et bibtex
avocs2012.pdf BibTex

Communications sans actes

Titre
TLA+ Proofs
Auteurs
Denis Cousineau; Damien Doligez; Leslie Lamport; Stephan Merz url; Daniel Ricketts; Hernán Vanzetto
Détail
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p.
Accès au bibtex
BibTex
Titre
Formal Verification Of Pastry Using TLA+
Auteurs
Tianxiang Lu; Stephan Merz url; Christoph Weidenbach
Détail
Leslie Lamport and Stephan Merz. International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France.
Accès au texte intégral et bibtex
paper.pdf paper.ps BibTex

2011

Communications avec actes

Titre
Towards Verification of the Pastry Protocol using TLA+
Auteurs
Stephan Merz; Tianxiang Lu; Christoph Weidenbach
Détail
R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. FMOODS/FORTE 2011, 6722
Accès au bibtex
BibTex

Communications sans actes

Titre
Towards certification of TLA+ proof obligations with SMT solvers
Auteurs
Stephan Merz url; Hernán Vanzetto
Détail
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wroclaw, Poland.
Accès au texte intégral et bibtex
tla2smt.pdf BibTex

2010

Communications avec actes

Titre
The TLA+ Proof System: Building a Heterogeneous Verification Platform
Auteurs
Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz
Détail
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, Theoretical Aspects of Computing – ICTAC 2010, 6255, pp. 44, Lecture Notes in Computer Science
Accès au bibtex
BibTex

2008

Communications sans actes

Titre
A TLA+ Proof System
Auteurs
Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz
Détail
Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar.
Accès au texte intégral et bibtex
main.pdf main.ps BibTex

Chapitres d’ouvrages scientifiques

Titre
The Specification Language TLA+
Auteurs
Stephan Merz
Détail
Dines Bjørner and Martin Henson. Logics of specification languages, Springer, pp. 401-452, 2008, Monographs in Theoretical Computer Science, 978-3-540-74106-0
Accès au bibtex
BibTex

The TLA+ proof system version 1.3.0 has been released!

It is available from the http://tla.msr-inria.inria.fr/tlaps/ home page