--- a/src/HOL/HoareParallel/document/root.tex Mon Sep 21 08:45:31 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-
-% $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}