tr.bib

@TECHREPORT{abrahammumm.deboer.deroever.steffen:multithreading-rep,
  AUTHOR = {Erika {\'A}brah{\'a}m-Mumm and {Frank S.} de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  TITLE = {Verification for {J}ava's Reentrant Multithreading
		  Concept: {S}oundness and Completeness},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t zu Kiel},
  YEAR = 2002,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-02-1},
  MONTH = MAR,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/02/tr-st-02-1.ps.gz},
  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 multithreaded programs, we introduce in
                  this paper  an \emph{assertional proof method} for safety
                  properties for \textsl{Java}$_{\mathsl{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.}
}

@TECHREPORT{abrahammumm.deboer.deroever.steffen:compositonalsemantics,
  AUTHOR = {Erika {\'A}brah{\'a}m-Mumm and {Frank S.} de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  TITLE = {A Compositional Operational Semantics for {Java$_\mathit{MT}$}},
  INSTITUTION = {Lehrstuhl f{\"ur} Software-Technologie,
                    Institut f{\"u}r Informatik und praktische Mathematik,
                    Christian-Albrechts-Universit{\"a}t zu Kiel},
  YEAR = 2002,
  TYPE = {Technical Report},
  NUMBER = {TR-ST-02-2},
  MONTH = MAY,
  URL = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/02/tr-st-02-2.ps.gz},
  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.} 
  
                  This report contains a compositional version of the
                  operational semantics of {\textsl{Java}$_\mathit{MT}$}.}
}