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;
     1

     2 % $Id$

     3

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

     5 \usepackage{graphicx}

     6 \usepackage[english]{babel}

     7 \usepackage{isabelle,isabellesym}

     8 \usepackage{pdfsetup}

     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

    21 \begin{abstract}\noindent

    22   In the following theories a formalization of the Owicki-Gries and

    23   the rely-guarantee 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{Prensa-PhD}.)  Using this formalizations we

    32   verify several non-trivial examples for parameterized and

    33   non-parameterized programs.  For the automatic generation of

    34   verification conditions with the Owicki-Gries method we define a

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

    36   verification of two garbage-collection algorithms, the second one

    37   parameterized in the number of mutators.

    38

    39 For excellent descriptions of this work see

    40 \cite{NipkowP-FASE99,PrenEsp00,Prensa-PhD,Prensa-ESOP03}.

    41

    42 \end{abstract}

    43

    44 \pagestyle{plain}

    45 \thispagestyle{empty}

    46 \tableofcontents

    47

    48 \clearpage

    49

    50 \begin{center}

    51   \includegraphics[scale=0.7]{session_graph}

    52 \end{center}

    53

    54 \newpage

    55

    56 \parindent 0pt\parskip 0.5ex

    57 \input{session}

    58

    59 \bibliographystyle{plain}

    60 \bibliography{root}

    61

    62 \end{document}