src/HOL/Hoare_Parallel/document/root.tex
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 32621 a073cb249a06
child 55369 713629c2b73c
permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
wenzelm@13033
     1
wenzelm@13033
     2
% $Id$
prensani@13021
     3
wenzelm@13106
     4
\documentclass[11pt,a4paper]{report}
wenzelm@13033
     5
\usepackage{graphicx}
prensani@13021
     6
\usepackage[english]{babel}
wenzelm@13033
     7
\usepackage{isabelle,isabellesym}
wenzelm@13033
     8
\usepackage{pdfsetup}
prensani@13021
     9
prensani@13021
    10
\urlstyle{rm}
prensani@13021
    11
\isabellestyle{it}
prensani@13021
    12
prensani@13021
    13
\renewcommand{\isamarkupheader}[1]{#1}
prensani@13021
    14
prensani@13021
    15
\begin{document}
prensani@13021
    16
prensani@13021
    17
\title{Hoare Logic for Parallel Programs}
prensani@13021
    18
\author{Leonor Prensa Nieto}
prensani@13021
    19
\maketitle
prensani@13021
    20
prensani@13099
    21
\begin{abstract}\noindent
prensani@13099
    22
  In the following theories a formalization of the Owicki-Gries and
prensani@13099
    23
  the rely-guarantee methods is presented. These methods are widely
prensani@13099
    24
  used for correctness proofs of parallel imperative programs with
prensani@13099
    25
  shared variables.  We define syntax, semantics and proof rules in
prensani@13099
    26
  Isabelle/HOL.  The proof rules also provide for programs
prensani@13099
    27
  parameterized in the number of parallel components. Their
prensani@13099
    28
  correctness w.r.t.\ the semantics is proven.  Completeness proofs
prensani@13099
    29
  for both methods are extended to the new case of parameterized
prensani@13099
    30
  programs. (These proofs have not been formalized in Isabelle. They
prensani@13099
    31
  can be found in~\cite{Prensa-PhD}.)  Using this formalizations we
prensani@13099
    32
  verify several non-trivial examples for parameterized and
prensani@13099
    33
  non-parameterized programs.  For the automatic generation of
prensani@13099
    34
  verification conditions with the Owicki-Gries method we define a
prensani@13099
    35
  tactic based on the proof rules.  The most involved examples are the
prensani@13099
    36
  verification of two garbage-collection algorithms, the second one
prensani@13099
    37
  parameterized in the number of mutators.
prensani@13099
    38
nipkow@19401
    39
For excellent descriptions of this work see
nipkow@19401
    40
\cite{NipkowP-FASE99,PrenEsp00,Prensa-PhD,Prensa-ESOP03}.
nipkow@19401
    41
prensani@13099
    42
\end{abstract}
prensani@13099
    43
prensani@13021
    44
\pagestyle{plain}
prensani@13021
    45
\thispagestyle{empty}
prensani@13021
    46
\tableofcontents
prensani@13021
    47
wenzelm@13036
    48
\clearpage
wenzelm@13036
    49
wenzelm@13033
    50
\begin{center}
wenzelm@13033
    51
  \includegraphics[scale=0.7]{session_graph}  
wenzelm@13033
    52
\end{center}
wenzelm@13033
    53
wenzelm@13033
    54
\newpage
wenzelm@13033
    55
prensani@13021
    56
\parindent 0pt\parskip 0.5ex
prensani@13021
    57
\input{session}
prensani@13021
    58
nipkow@19401
    59
\bibliographystyle{plain}
nipkow@19401
    60
\bibliography{root}
prensani@13021
    61
prensani@13021
    62
\end{document}