db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
@InProceedings{Welch11,
  title =        "{A}dding {F}ormal {V}erification to occam-\&amp;pi;",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
  author=        "Welch, Peter H. and Pedersen,  Jan Bækgaard and Barnes,  Frederick R. M. and Ritson,  Carl G. and Brown,  Neil C.C.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
  editor=        "Welch, Peter H. and Sampson,  Adam T. and Pedersen,  Jan Bækgaard and Kerridge,  Jon and Broenink,  Jan F. and Barnes,  Frederick R. M.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
  pages =        "379--379",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2011",
  isbn=          "978-1-60750-773-4",
  year=          "2011",
  month=         "jun",
  abstract=      "This is a proposal for the formal verification of
     occam-\&amp;pi;
programs to be managed entirely within
     occam-\&amp;pi;.
The language is extended with qualifiers on
     types and processes
(to indicate relevance for verification
     and/or execution) and assertions
about refinement (including
     deadlock, livelock and determinism).
The compiler abstracts
     a set of CSPm equations and assertions,
delegates their
     analysis to the FDR2 model checker and reports back
in terms
     related to the occam-\&amp;pi; source.
The rules for mapping
     the extended occam-\&amp;pi; to CSPm are given.
The full
     range of CSPm assertions is accessible, with no knowledge
     of
CSP formalism required by the occam-\&amp;pi; programmer.
      Programs are proved
just by
     \textlessem\textgreaterwriting\textless/em\textgreater and
     \textlessem\textgreatercompiling\textless/em\textgreater
     programs.
A case-study analysing a new (and elegant)
     solution to the
     \textlessem\textgreaterDining
Philosophers\textless/em\textgreater
     problem is presented.
Deadlock-freedom for colleges with
     \textlessem\textgreaterany\textless/em\textgreater number of
     philosphers
is established by verifying an induction
     argument (the base and
induction steps).
Finally, following
     guidelines laid down by Roscoe, the careful use
     of
\textlessem\textgreatermodel
     compression\textless/em\textgreater is demonstrated to
     verify directly the deadlock-freedom
of an occam-\&amp;pi;
     college with 10\^{}2000 philosphers (in around 30
     seconds).
All we need is a universe large enough to contain
     the computer
on which to run it."
}