--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare_Parallel/document/root.tex Mon Sep 21 10:58:25 2009 +0200
@@ -0,0 +1,62 @@
+
+% $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}