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}