TLA+ as an Isabelle object logic
- Domains
- verification, theorem proving
- Proposed by
- Stephan Merz
- Institute
- LORIA,
Nancy, France
in cooperation with the
Joint Centre
Microsoft Research - INRIA (Saclay, France)
- Duration
- 3-6 months, spring or summer 2009
Context
TLA+
is a language for specifying and verifying concurrent
and distributed systems. It is based on a variant of Zermelo-Fränkel
set theory for describing the data structures manipulated by the
algorithms to be verified, and on the Temporal Logic of Actions (TLA)
for describing their dynamic behavior. An extended version of TLA+
(called TLA+2) allows writing proofs in a hierarchical style, and
efforts are underway in the project
Tools and Methodologies for Formal Specifications and for Proofs
to implement a system around a Proof Manager that invokes
back-end provers such as
Zenon and
haRVey to check those proofs.
More specifically, the Proof Manager computes proof obligations that
establish the correctness of the proof and sends them to one or more
back-end provers to be verified. We rely on back-end provers that are
proof-producing, i.e. they output a proof trace that can be certified in a
logical framework such as
Isabelle. In this way, the
kernel of the logical framework becomes the only trusted component of
the TLA+ proof system.
Subject
The core of the TLA+ specification language has been encoded in
Isabelle as a new object logic, and the main existing semi-automatic
proof methods of Isabelle (including rewriting and tableau- and
resolution-based theorem proving) have been instantiated for TLA+. The
currently supported subset includes propositional and first-order
logic, elementary set theory, functions, fixed points, and the
construction of natural numbers. The subject of this internship is to
extend Isabelle/TLA+ by providing support for further theories such as
elementary arithmetic, strings, tuples, sequences, and records.
Depending on the length of the internship and the interests of the
candidate, the integration of further back-end provers such as
haRVey and
Metis
can also be envisaged. The intern will contribute
to the validation of the interaction between the Proof Manager and
Isabelle/TLA+ by carrying out small case studies in interaction with
the developers of the overall proof system.
The verification of distributed and concurrent algorithms is an
important research problem, to which the TLA+ prover project aims to
contribute. The internship could therefore naturally give rise to a
future thesis.
Prerequisites
The proposed subject requires strong interest in formal approaches to
system specification and verification. Experience with an interactive
proof assistant (such as Isabelle, HOL or Coq) would be welcome.
Detailed knowledge of Isabelle is not required and can be acquired
during the internship.
References
T. Nipkow, L. Paulson, M. Wenzel:
Isabelle/HOL. A Proof Assistant for Higher-Order Logic.
Lecture Notes in Computer Science, vol. 2283. Springer, 2002.
Available from the Isabelle web page.
L. Lamport:
Specifying Systems.
Addison-Wesley, Boston, Mass., 2002.
[Web page]
K. Chaudhuri, D. Doligez, L. Lamport, S. Merz:
A TLA+ Proof System.
Submitted. [pdf]
Stephan Merz