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

Communication dans un congrès

titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
article
ARQNL 2014 – Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-01063512/file/final.pdf BibTex
titre
Refinement Types for TLA+
auteur
Stephan Merz, Hernán Vanzetto
article
Julia M. Badger and Kristin Yvonne Rozier. NASA Formal Methods – 6th International Symposium, 2014, Houston, Texas, United States. Springer, 8430, pp.143-157, LNCS. <10.1007/978-3-319-06200-6_11>
Accès au bibtex
BibTex

2012

Communication dans un congrès

titre
Formal Verification Of Pastry Using TLA+
auteur
Tianxiang Lu, Stephan Merz, Christoph Weidenbach
article
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
http://hal.inria.fr/hal-00768812/file/paper.pdf BibTex
titre
Harnessing SMT Solvers for TLA+ Proofs
auteur
Stephan Merz, Hernán Vanzetto
article
Gerald Lüttgen and Stephan Merz. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany. EASST, 53, ECEASST; Automated Verification of Critical Systems (AVoCS 2012)
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00760579/file/avocs2012.pdf BibTex
titre
Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
auteur
Stephan Merz, Hernán Vanzetto
article
Nikolaj Bjørner and Andrei Voronkov. 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. Springer, 7180, pp.289-303, Lecture Notes in Computer Science; Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2012). <10.1007/978-3-642-28717-6_23>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00760570/file/tla2smt.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods – FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, Lecture Notes in Computer Science; FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings. <10.1007/978-3-642-32759-9_14>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00726631/file/final.pdf BibTex
titre
TLA+ Proofs
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
article
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p., <http://arxiv.org/abs/1208.5933>
Accès au bibtex
BibTex

2011

Communication dans un congrès

titre
Towards Verification of the Pastry Protocol using TLA+
auteur
Stephan Merz, Tianxiang Lu, Christoph Weidenbach
article
R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. 6722, FMOODS/FORTE 2011
Accès au bibtex
BibTex
titre
Towards certification of TLA+ proof obligations with SMT solvers
auteur
Stephan Merz, Hernán Vanzetto
article
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving – PxTP 2011, Aug 2011, Wroclaw, Poland. <http://pxtp2011.loria.fr>
Accès au texte intégral et bibtex
http://hal.inria.fr/hal-00645458/file/tla2smt.pdf BibTex

2010

Communication dans un congrès

titre
The TLA+ Proof System: Building a Heterogeneous Verification Platform
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
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, Lecture Notes in Computer Science; Theoretical Aspects of Computing – ICTAC 2010. <10.1007/978-3-642-14808-8_3>
Accès au bibtex
BibTex

2008

Communication dans un congrès

titre
A TLA+ Proof System
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
article
Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar
Accès au texte intégral et bibtex
http://hal.inria.fr/inria-00338299/file/main.pdf BibTex

Chapitre d’ouvrage

titre
The Specification Language TLA+
auteur
Stephan Merz
article
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