Supplementary material on the design of TLAPS
The TLA+ Proof System is developed at the Joint Centre of Microsoft Research and
Inria in Saclay. The main home page is
here;
it contains the links for downloading TLAPS as well as documentation
relevant for users.
This page collects supplementary information of use for developers, on the
design of TLAPS and some of its back-end provers.
The SMT Backend
The SMT backend is the main workhorse of TLAPS and is by default called first on
every proof obligation. Its design is described in the papers listed below, and
more details appear in Hernán Vanzetto's PhD thesis. A variant of the
backend can be used to produce input in TPTP-FOF format for use with automated
first-order provers such as E or Spass. The translation from TLA+ set theory to
(possibly multi-sorted) first-order logic relies on rewriting rules documented
here.
Some case studies demonstrating the reduction in proof size obtained thanks to
the SMT backend are also available:
[ Memoir | Paxos ]
References
- Stephan Merz, Hernán Vanzetto.
Automatic Verification Of TLA+ Proof Obligations With SMT Solvers.
18th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18).
© Springer, LNCS 7180, pp. 289-303 (2012).
[PDF
| Springer Link]
- Stephan Merz, Hernán Vanzetto.
Encoding TLA+ into Many-Sorted First-Order Logic.
5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016).
© Springer, LNCS 9675, pp. 54-69 (2016).
[PDF
| Springer Link]
- Stephan Merz, Hernán Vanzetto.
Refinement Types for TLA+.
6th Intl. Symp. NASA Formal Methods (NFM 2014).
© Springer, LNCS 8430, pp. 143-157 (2014).
[PDF
| Springer Link]
- Hernán Vanzetto.
Proof Automation and Type Synthesis for Set Theory in the Context of TLA+.
PhD thesis, Université de Lorraine, 2014.
The Isabelle Backend
Isabelle/TLA+ is a faithful encoding of the set theory of TLA+ as an object
logic in the proof assistant Isabelle. Pretty-printed versions of the Isabelle
theories making up the encoding are available here.
The sources of the Isabelle theories are part of the TLAPS distribution and are
therefore not replicated here.
Stephan Merz