src/HOL/Hoare_Parallel/document/root.tex

+
+% $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}