%%% -*- mode: LaTeX; TeX-master: "main.tex"; -*-

\ifx\master\undefined
\documentclass[a4paper]{easychair}
\usepackage{submission}
\begin{document}
{\let\master\relax\input{frontmatter}}
\fi
%%%% PLEASE DO NOT EDIT ABOVE THIS LINE

\section{Introduction}
\label{sec:intro}

\tlaplus\ is a language for specifying the behaviour of concurrent and
distributed systems and asserting properties of those
systems~\cite{lamport03tla}.  However, it provides no way to write
proofs of those properties.  We have designed an extended version of
the language that allows writing proofs, and we have begun
implementing a system centered around a \textit{Proof Manager} (\PM)
that invokes existing automated and interactive proof systems to check
those proofs. For now, the new version of \tlaplus\ is called \tlatwo\
to distinguish it from the current one.  We describe here the \tlatwo
proof constructs and the current state of the proof system.

The primary goal of \tlatwo\ and the proof system is the mechanical
verification of systems specifications. The proof system must not only
support the modal and temporal aspects of TLA needed
to reason about system properties, but must also support
ordinary mathematical reasoning in the underlying logic. Proofs in
\tlatwo are natural deduction proofs written in a hierarchical style
that we have found to be good for ordinary
mathematics~\cite{lamport93amm} and crucial for managing the
complexity of correctness proofs of systems~\cite{gafni:disk-paxos}.

The \PM\ computes proof obligations that establish the correctness of
the proof and sends them to one or more back-end provers to be
verified.  Currently, the back-end provers are Isabelle/\tlaplus, a
faithful axiomatisation of \tlaplus\ in Isabelle/Pure, and
Zenon~\cite{bonichon07lpar}, a tableau prover for classical
first-order logic with equality.  The \PM\ first sends a proof
obligation to Zenon.  If Zenon succeeds, it produces an Isar script
that the \PM\ sends to Isabelle to certify.  Otherwise, the \PM
directs Isabelle to try to find a proof with its automated tactics.
In both cases, the proofs are certified by Isabelle/\tlaplus.
%%
%% SM: I changed the following sentence because its original
%% formulation seems to defeat certifiability, an issue that we
%% highlight.
%%
%This system
%architecture allows us in the future to add other back-end provers
%whose proofs need not be certified by Isabelle/\tlaplus.
The system architecture easily accomodates other back-end provers; if
these are proof-producing, certification by Isabelle/\tlaplus\ gives
us high high confidence in the overall correctness.

The \tlatwo\ proof constructs are described in
Section~\ref{sec:proof-language}.  Section~\ref{sec:obligations}
describes the proof obligations generated by the \PM, and
Section~\ref{sec:backend} describes how the \PM\ uses Zenon and
Isabelle to verify them.  The conclusion summarizes what we have done
and not yet done and briefly discusses related work.

%%%% PLEASE DO NOT EDIT BELOW THIS LINE
\ifx\master\undefined
{\let\master\relax\input{rearmatter}}
\end{document}
\fi
