The Theory and Practice of Concurrency

Papers and Theses

This page gives access to some papers and theses on topics related to the book. Note that some further papers related to example files can be found in the examples section of this web-site.


Bryan Scattergood (Oxford University D.Phil, 1998) The semantics and implementation of machine-readable CSP

Lars Wulf (Oxford University D.Phil, 1997) Interaction and security in distributed computing (see also the related example files obtainable here)

Ranko Lazic (Oxford University D.Phil, 1999, complete draft) A semantic study of data independence with applications to model checking


Maintaining consistency in distributed databases by A.W. Roscoe (background material for Section 15.2.1)

Verifying an infinite family of inductions simultaneously using data independence and FDR by S.J. Creese and A.W. Roscoe (techniques that exploit the ideas of Section 15.2.2 to give further methods for dealing with scaleability).

Proving security protocols with model checkers by data independence techniques by A.W. Roscoe and P.J. Broadfoot (Combining the ideas of Sections 15.2 and 15.3 to give general proofs of cryptographic protocols.)

Noninterference properties for nondeterministic processes by R Forster (about some extensions of the information flow material in Section 12.4 to nondeterministic processes).

What is intransitive noninterference? by A.W. Roscoe and M.H. Goldsmith (Extending the ideas about information flow given in Section 12.4 to handle intransitive security policies from examples such as downgraders: there may be three users where information can flow from A to B and from B to C, but not from A to C.)

Research Proposal

Exploiting Data Independence by R.S. Lazic and A.W. Roscoe