@InProceedings{WelchMartin00,
  title =        "{F}ormal {A}nalysis of {C}oncurrent {J}ava {S}ystems",
  author=        "Welch, Peter H. and Martin,  Jeremy M. R.",
  editor=        "Welch, Peter H. and Bakkers,  Andr\`{e} W. P.",
  pages =        "275--301",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2000",
  isbn=          "1 58603 077 9",
  year=          "2000",
  month=         "sep",
  abstract=      "Java threads are synchronised through primitives based upon
     monitor concepts developed in the early 1970s. The semantics
     of Java's primitives have only been presented in natural
     language -- this paper remedies this with a simple and
     formal CSP model. In view of the difficulties encountered in
     reasoning about any non-trivial interactions between Java
     threads, being able to perform that reasoning in a formal
     context (where careless errors can be highlighted by
     mechanical checks) should be a considerable confidence
     boost. Further, automated model-checking tools can be used
     to root out dangerous states (such as deadlock and
     livelock), find overlooked race hazards and prove
     equivalence between algorithms (e.g. between optimised and
     unoptimised versions). A case study using the CSP model to
     prove the correctness of the JCSP and CTJ channel
     implementations (which are built using standard Java monitor
     synchronisation) is presented. In addition, the JCSP
     mechanism for ALTing (i.e. waiting for and, then, choosing
     between multiple events) is verified. Given the history of
     erroneous implementations of this key primitive, this is a
     considerable relief."
}