author | wenzelm |
Thu, 22 Apr 2021 10:11:11 +0200 | |
changeset 73595 | aece5cc9efb7 |
parent 58884 | be4d203d35b3 |
permissions | -rw-r--r-- |
13106 | 1 |
\documentclass[11pt,a4paper]{report} |
73595
aece5cc9efb7
simplified typesetting of \<guillemotleft>...\<guillemotright>;
wenzelm
parents:
58884
diff
changeset
|
2 |
\usepackage[T1]{fontenc} |
13033 | 3 |
\usepackage{graphicx} |
4 |
\usepackage{isabelle,isabellesym} |
|
5 |
\usepackage{pdfsetup} |
|
13021 | 6 |
|
7 |
\urlstyle{rm} |
|
8 |
\isabellestyle{it} |
|
9 |
||
10 |
\begin{document} |
|
11 |
||
12 |
\title{Hoare Logic for Parallel Programs} |
|
13 |
\author{Leonor Prensa Nieto} |
|
14 |
\maketitle |
|
15 |
||
13099 | 16 |
\begin{abstract}\noindent |
17 |
In the following theories a formalization of the Owicki-Gries and |
|
18 |
the rely-guarantee methods is presented. These methods are widely |
|
19 |
used for correctness proofs of parallel imperative programs with |
|
20 |
shared variables. We define syntax, semantics and proof rules in |
|
21 |
Isabelle/HOL. The proof rules also provide for programs |
|
22 |
parameterized in the number of parallel components. Their |
|
23 |
correctness w.r.t.\ the semantics is proven. Completeness proofs |
|
24 |
for both methods are extended to the new case of parameterized |
|
25 |
programs. (These proofs have not been formalized in Isabelle. They |
|
26 |
can be found in~\cite{Prensa-PhD}.) Using this formalizations we |
|
27 |
verify several non-trivial examples for parameterized and |
|
28 |
non-parameterized programs. For the automatic generation of |
|
29 |
verification conditions with the Owicki-Gries method we define a |
|
30 |
tactic based on the proof rules. The most involved examples are the |
|
31 |
verification of two garbage-collection algorithms, the second one |
|
32 |
parameterized in the number of mutators. |
|
33 |
||
19401 | 34 |
For excellent descriptions of this work see |
35 |
\cite{NipkowP-FASE99,PrenEsp00,Prensa-PhD,Prensa-ESOP03}. |
|
36 |
||
13099 | 37 |
\end{abstract} |
38 |
||
13021 | 39 |
\pagestyle{plain} |
40 |
\thispagestyle{empty} |
|
41 |
\tableofcontents |
|
42 |
||
13036 | 43 |
\clearpage |
44 |
||
13033 | 45 |
\begin{center} |
46 |
\includegraphics[scale=0.7]{session_graph} |
|
47 |
\end{center} |
|
48 |
||
49 |
\newpage |
|
50 |
||
13021 | 51 |
\parindent 0pt\parskip 0.5ex |
52 |
\input{session} |
|
53 |
||
19401 | 54 |
\bibliographystyle{plain} |
55 |
\bibliography{root} |
|
13021 | 56 |
|
57 |
\end{document} |