13033

1 


2 
% $Id$

13021

3 

13106

4 
\documentclass[11pt,a4paper]{report}

13033

5 
\usepackage{graphicx}

13021

6 
\usepackage[english]{babel}

13033

7 
\usepackage{isabelle,isabellesym}


8 
\usepackage{pdfsetup}

13021

9 


10 
\urlstyle{rm}


11 
\isabellestyle{it}


12 


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


14 


15 
\begin{document}


16 


17 
\title{Hoare Logic for Parallel Programs}


18 
\author{Leonor Prensa Nieto}


19 
\maketitle


20 

13099

21 
\begin{abstract}\noindent


22 
In the following theories a formalization of the OwickiGries and


23 
the relyguarantee methods is presented. These methods are widely


24 
used for correctness proofs of parallel imperative programs with


25 
shared variables. We define syntax, semantics and proof rules in


26 
Isabelle/HOL. The proof rules also provide for programs


27 
parameterized in the number of parallel components. Their


28 
correctness w.r.t.\ the semantics is proven. Completeness proofs


29 
for both methods are extended to the new case of parameterized


30 
programs. (These proofs have not been formalized in Isabelle. They


31 
can be found in~\cite{PrensaPhD}.) Using this formalizations we


32 
verify several nontrivial examples for parameterized and


33 
nonparameterized programs. For the automatic generation of


34 
verification conditions with the OwickiGries method we define a


35 
tactic based on the proof rules. The most involved examples are the


36 
verification of two garbagecollection algorithms, the second one


37 
parameterized in the number of mutators.


38 

19401

39 
For excellent descriptions of this work see


40 
\cite{NipkowPFASE99,PrenEsp00,PrensaPhD,PrensaESOP03}.


41 

13099

42 
\end{abstract}


43 

13021

44 
\pagestyle{plain}


45 
\thispagestyle{empty}


46 
\tableofcontents


47 

13036

48 
\clearpage


49 

13033

50 
\begin{center}


51 
\includegraphics[scale=0.7]{session_graph}


52 
\end{center}


53 


54 
\newpage


55 

13021

56 
\parindent 0pt\parskip 0.5ex


57 
\input{session}


58 

19401

59 
\bibliographystyle{plain}


60 
\bibliography{root}

13021

61 


62 
\end{document}
