src/HOL/HoareParallel/document/root.tex

moved lemma all_not_ex to HOL.thy ; tuned proofs

% $Id$

\documentclass[11pt,a4paper]{report}
\usepackage{graphicx}
\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}

\urlstyle{rm}
\isabellestyle{it}

\renewcommand{\isamarkupheader}[1]{#1}

\begin{document}

\title{Hoare Logic for Parallel Programs}
\author{Leonor Prensa Nieto}
\maketitle

\begin{abstract}\noindent
  In the following theories a formalization of the Owicki-Gries and
  the rely-guarantee methods is presented. These methods are widely
  used for correctness proofs of parallel imperative programs with
  shared variables.  We define syntax, semantics and proof rules in
  Isabelle/HOL.  The proof rules also provide for programs
  parameterized in the number of parallel components. Their
  correctness w.r.t.\ the semantics is proven.  Completeness proofs
  for both methods are extended to the new case of parameterized
  programs. (These proofs have not been formalized in Isabelle. They
  can be found in~\cite{Prensa-PhD}.)  Using this formalizations we
  verify several non-trivial examples for parameterized and
  non-parameterized programs.  For the automatic generation of
  verification conditions with the Owicki-Gries method we define a
  tactic based on the proof rules.  The most involved examples are the
  verification of two garbage-collection algorithms, the second one
  parameterized in the number of mutators.

For excellent descriptions of this work see
\cite{NipkowP-FASE99,PrenEsp00,Prensa-PhD,Prensa-ESOP03}.

\end{abstract}

\pagestyle{plain}
\thispagestyle{empty}
\tableofcontents

\clearpage

\begin{center}
  \includegraphics[scale=0.7]{session_graph}  
\end{center}

\newpage

\parindent 0pt\parskip 0.5ex
\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}