tr.bib

@TECHREPORT{abraham.deboer.deroever.steffen:hoarelogic-rep,
  AUTHOR = {Erika {\'A}brah{\'a}m and {Frank S.} de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  TITLE = {A {H}oare Logic for Monitors in {J}ava},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t zu Kiel},
  YEAR = 2003,
  TYPE = {Techical report},
  NUMBER = {TR-ST-03-1},
  MONTH = APR,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/02/tr-st-03-1.pdf},
  ABSTRACT = {Besides the features of a class-based object-oriented
                  language, \textsl{Java} integrates concurrency via its
                  thread-classes, allowing for a \emph{multithreaded} flow
                  of control.  The concurrency model includes
                  \emph{shared-variable} concurrency via instance
                  variables, \emph{coordination} via reentrant
                  synchronization monitors, \emph{synchronous message
                  passing,} and dynamic \emph{thread creation.}

  
                  To reason about safety-properties of multithreaded
                  programs, we introduce in this paper a tool-supported
                  \emph{assertional proof method} for \textsl{Java}$_\mathit{MT}$
                  (``\emph{Multi-Threaded Java}''), a small concurrent
                  sublanguage of \textsl{Java}, covering the mentioned concurrency
                  issues as well as the object-based core of \textsl{Java}, i.e.,
                  object creation, side effects, and aliasing, but leaving
                  aside inheritance and subtyping.  We show soundness and
                  relative completeness of the proof method.}
}