Publications:
Notes on Domain Theory
PDF
 A theory of communicating sequential processes, Oxford University Computing
Laboratory technical monograph PRG16, May 1981
(with S.D. Brookes and C. A. R. Hoare) PDF
 A mathematical theory of communicating processes, Oxford University D. Phil.
thesis, 1982. PDF Please note this is a 270 page,
118 Mb scanned file and will take some time to download.
 Criteria for metrisability, Proc. Amer. Math. Soc. 90 (April 1984),
631640 (with P.J. Collins) http
 A theory of communicating sequential processes, Journal of the ACM 31,
No. 3 (July 1984), 560599 (with S.D. Brookes and C.A.R. Hoare)
PDF
 Programs as executable predicates, Proceedings of FGCS84 (ICOT, editors)
220228 (with C.A.R. Hoare).
PDF
 Continuous analogues of axiomatised digital surfaces,
Computer Vision, Graphics and Image Processing 29
(January 1985), 6086 (with T.Y. Kong).
PDF
 A lattice of conditions on topological spaces, Proc. Amer.
Math. Soc. 94 (July 1985), 487496 (with P.J. Collins, G.M. Reed and M.E. Rudin)
http
 Proceedings of the Pittsburgh seminar on concurrency, Springer
LNCS 197 (1985) (coeditor with S.D. Brookes and G. Winskel).
http
 An improved failures model for communicating processes, in Proceedings of
the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 281305
(with S.D. Brookes). PDF
 Denotational semantics for occam, in Proceedings of the Pittsburgh seminar
on concurrency, Springer LNCS 197 (1985), 306329.
PDF
 Deadlock analysis in networks of communicating processes, in Logics and
Models of Concurrent Systems (ed. K.R. Apt) NATO ASI series F, Vol. 13, Springer 1985,
305324 (with S.D. Brookes).
 Characterisations of simplyconnected finite polyhedra in 3space, Bull.
London Math. Soc. 17 (November 1985), 575578 (with T.Y. Kong).
PDF
 A theory of binary digital pictures, Computer Vision, Graphics and
Image Processing 32 (November 1985), 221243 (with T.Y. Kong).
PDF
 Specifying problem one using the failures model for CSP and deriving CSP
processes which meet this specification, in The Analysis of Concurrent Systems
(ed. B.T. Denvir et al), Springer LNCS 207 (1985), 103109.
PDF
 A CSP solution to the ``trains'' problem, in The Analysis of
Concurrent Systems (ed. B.T. Denvir et al), Springer LNCS 207 (1985), 384388.
PDF
 Local symmetry and triangle laws are sufficient for metrisability,
Colloquia Mathematica Societatis Janos Bolyai 41, 177181
(with P.J. Collins). PDF
 A timed model for communicating sequential processes, Proc.ICALP 86,
Springer LNCS 226 (1986), 314323 (with G.M. Reed).PDF
 The pursuit of deadlock freedom, Information and Computation 75,
3 (December 1987), 289327 (with Naiem Dathi).
PS
 Metric spaces as models for realtime concurrency, in Main
et al, eds. Proceedings of the Third Workshop on the Mathematical Foundations
of Programming Language Semantics (New Orleans, 1987) Springer LNCS 298 (1988), 331343
(with G.M. Reed).PDF
 Laws of programming, Communications of the ACM 30, 8
(August 1987), 672686 (with C.A.R. Hoare, He Jifeng, I.J. Hayes, C.C. Morgan,
J.W. Sanders, I.H. Sorensen, J.M. Spivey and B.A. Sufrin).
(Previously appeared as Oxford University Computing Laboratory Technical Report PRG42.)
PDF
 Routing messages through networks: an exercise in deadlock avoidance,
in Muntean ed. et al. Programming of Transputer Based Machines: Proceedings of {7}th
occam User Group Technical Meeting, (1416 September 1987, Grenoble, France),
IOS B.V., Amsterdam.
PS
 Transforming occam programs, in The Design and Application of Parallel
Digital Processors (IEE Conference Publication 298) (1988) (with M.H. Goldsmith).
PDF
 A timed model for communicating sequential processes, Theoretical
Computer Science 58 (1988), 249261 (with G.M. Reed).
PDF
 The laws of occam programming, Theoretical Computer Science 60 (1988),
177229 (with C.A.R. Hoare). (Previously appeared as Oxford University Computing Laboratory
Technical Report PRG53, 1986.) PDF
 The decomposition of a rectangle into rectangles of minimal perimeter,
University of Maryland Center for Automation Research CARTR169 (1986)
(with T.Y. Kong and D.M. Mount) (Also SIAM Journal of Computing 17, 6 pp12151231.)
PDF
 An Operational Semantics for CSP (with S. D. Brookes and D. J. Walker)
Technical Report 1986 PS
 An alternative order for the failures model, in `Two papers on CSP',
technical monograph PRG67, Oxford University Computing Laboratory, July 1988.
Also appeared in Journal of Logic and Computation 2, 5 pp557577.
PS
 Unbounded nondeterminism in CSP, in `Two papers on CSP', technical monograph
PRG67, Oxford University Computing Laboratory, July 1988.
Also Journal of Logic and Computation, Vol 3, No 2 pp131172 (1993).
PS
 Unbounded nondeterminism in CSP (with G.Barrett), in the Proceedings of MFPS89
(Springer LNCS 298). PS
PDF
 Deadlock analysis in networks of communicating processes
(with S.D. Brookes) Distributed Computing (1991) 4 209230.
PDF
 A lattice of conditions on topological spaces II
(with P. Moody, G.M. Reed and P.J. Collins) Fundamenta Mathematicae 138 (1991)
pp6981 PDF
 The pointcountable base problem, (with P.J. Collins and G.M. Reed)
in `Problems in Topology' (G.M. Reed and J. van Mill, eds) Elsevier 1990.
PDF
 Maintaining consistency in distributed databases, Technical Monograph PRG87,
Oxford University Computing Laboratory (1990).
PS
 Communication and correctness in Timed CSP,
(with S.A. Schneider, J.W. Davies, D.M. Jackson, and G.M. Reed),
Technical Report to Esprit SPEC project, 1990.
 A temporal logic for Timed CSP (with D.M. Jackson, J.W. Davies, G.M. Reed,
and S.A. Schneider), Technical Report to Esprit SPEC project, 1990.
 Topology, computer science and the mathematics of convergence,
in Topology and Category Theory in Computer Science (Reed, Roscoe, Wachter, eds)
OUP 1991. PS
 Topology and category theory in computer science, (coedited with G.M. Reed
and R.F. Wachter) OUP 1991, (proceedings of a special session at the 1989
Oxford Topology Conference).
 Analysing TM_{FS}: a study of nondeterminism in realtime
concurrency (with G.M. Reed), in Concurrency: Theory Language and Architecture,
(Yonezawa and Ito, eds) Springer LNCS 491.
PS
 CSP and timewise refinement (with G. M. Reed and S. A. Schneider),
Proceedings of the BCSFACS Refinement Workshop (Cambridge, 1991), LNCS.
 Star covering properties (with E.K. van Douwen, G.M. Reed and I.J. Tree)
Topology and its Applications 39 (1991) 71103.
PDF
 Formal methods in the development of the H1 Transputer
(with A.D.B. Cox, M.H. Goldsmith and J.B. Scattergood), in Proceedings of Transputing
91 (IOS).
 Concepts of digital topology (with T.Y. Kong)
Topology and its applications 46 (1992) 219262.
PDF
 Timed CSP: theory and practice
(with J.Davies, D.Jackson, G.M.Reed, J.Reed and S.A. Schneider),
Proceedings of REX Workshop, LNCS 600 (1992).
 Acyclic monotone normality (with P. Moody),
Topology and its Applications 47 (1992) 5367.
PDF
 Occam in the specification and verification of microprocessors
Phil Trans R. Soc. Lond A (1992) 339, 137151. Also in Mechanised Reasoning
and Hardware Design, M.J.C. Gordon and C.A.R. Hoare, eds (PrenticeHall, 1992).
Original paper http
Extended Version PS
 A semantic model for occam II (with M.H. Goldsmith and B.G.O. Scott)
Proceedings of Transputing 93.
 Denotational semantics for occam II (with M.H. Goldsmith and B.G.O. Scott)
Oxford University Computing Laboratory Technical monograph PRG108 (1993).
PDF
 Developing and verifying protocols in CSP,
Proceedings of Mierlo workshop on protocols, published by TU Eindhoven.
 Fixed points without completeness (with M.W. Mislove and S.A. Schneider),
Theoretical Computer Science 138, 2 pp273314.
 Modelchecking CSP, In A Classical Mind: essays in Honour of
C.A.R. Hoare, PrenticeHall 1994.
PS
 A Classical Mind: essays in Honour of C.A.R. Hoare, PrenticeHall 1994
(editor).
 Denotational semantics for occam2, Part 1 (
with M.H. Goldsmith and B.G.O. Scott) Transputer Communications 1, 2 pp6591.
 Denotational semantics for occam2, Part 2
(with M.H. Goldsmith and B.G.O. Scott) Transputer Communications 2. 1 pp2567.
 Noninterference through determinism (with J.C.P. Woodcock and L Wulf)
in proceedings of ESORICS 94 (LNCS 875).PDF
 Noninterference through determinism (with J.C.P. Woodcock and L Wulf)
(revised version of above) Journal of Computer Security 4, 1 (pp2754), 1996.
PDF
 CSP and determinism in security modelling Proceedings of 1995 IEEE
Symposium on Security and Privacy (IEEE Computer Society Press)
PS
 Composing and decomposing systems under security properties (with L. Wulf)
Proceedings of 1995 IEEE Computer Security Foundations Workshop
(IEEE Computer Society Press) PS
 Modelling and verifying keyexchange protocols using CSP and FDR
Proceedings of 1995 IEEE Computer Security Foundations Workshop
(IEEE Computer Society Press) PS
 Hierarchical compression for modelchecking CSP,
or How to check 10^{20} dining philosophers for deadlock
(with P.H.B. Gardiner, M.H. Goldsmith, J.R. Hulance, D.M.Jackson and J.B. Scattergood)
In proceedings of TACAS 1995 (BRICS; also, revised, in a version of these proceedings
published by LNCS) PS
PDF
 The timed failuresstability model for Timed CSP
(with G.M. Reed) Oxford University Computing Laboratory Technical Monograph PRG119 (1996)`,
also appeared in Theoretical Computer Science, Vol 211 (1999).
PS
PDF
 Intensional specifications of security protocols
Proceedings of 1996 IEEE Computer Security Foundations Workshop
(IEEE Computer Society Press) PS
 On transition systems and nonwellfounded sets,
(with R.S. Lazic) Annals of the New York Academiy of Sciences Vol 806,
1996. PS
PDF
 The perfect spy for modelchecking cryptoprotocols,
(with M.H. Goldsmith)} Proceedings of DIMACS workshop on the design and formal
verification of cryptoprotocols, 1997.
(http://dimacs.rutgers.edu/workshops/program2/program.html)
PDF
 A Case Study of the Formal Specification of a Parallel System using CSP,
(with S. Kiyamura) in "Correct Models of Parallel Computing"' (S. Noguchi and M. Ota, eds), IOS Press 1997
 Using CSP to detect errors in the TMN protocol (with G. Lowe)
University of Leicester Technical Report (1996) and
IEEE transactions on Software Engineering Vol 23 (1997)
PS
 Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays,
(with R. Lazic) Proceedings of INFINITY'98, Aalborg, Denmark, July 1998, extended version as
Oxford University Computing Laboratory TR298.
PS
(66a) Extended Abstract as above
ps file
 Proving security protocols with model checkers by data independence techniques
Proceedings of CSFW 1998, IEEE Press. PS
PDF
 The theory and practice of concurrency, Prentice Hall, 1998,
ISBN 01367744095, pp. xv+565.amended 2005
PS
PDF
 What is intransitive noninterference? Proceedings of CSFW 1999, IEEE Press.
(with M.H. Goldsmith) PS
 Proving security protocols with model checkers by data independence techniques,
(with P.J. Broadfoot) Journal of Computer Security Vol 7 (1999)
PS
PDF
 Data independence with predicate symbols, (with R.S. Lazic)
Proceedings of the International Conference on Parallel and Distributed Processing
Techniques and Applications (PDPTA'99), June 28  July 1 1999, Las Vegas, Nevada, USA. Volume I.
Published by CSREA Press.
PS
 Verifying an infinite family of inductions simultaneously using data
independence and FDR, (with S.J. Creese) In Formal Methods for Protocol Engineering
and Distributed Systems, the proceedings of Formal Description Techniques for Distributed
Systems and Communication Protocols and Protocol Specification, Testing and Verification
(FORTE/PSTV'99), October 58 1999, Beijing, China.
Published by Kluwer Academic Publishers. PS
PDF
 Formal Verification of Arbitrary Network Topologies, (with S.J. Creese)
Proceedings of the International Conference on Parallel and Distributed Processing
Techniques and Applications (PDPTA'99), June 28  July 1 1999, Las Vegas, Nevada, USA.
Volume II. Published by CSREA Press.
PS
PDF
 TTP: A case study in combining induction and data independence,
(with S.J. Creese) Oxford University Computing Laboratory Technical Report, PRGTR199.
PS
 Data independent induction over structured networks, (with S.J. Creese)
Proceedings of PDPTA2000 PS
 Automating Data Independence, (with P.J. Broadfoot and G. Lowe)
Proceedings of ESORICS2000, LNCS 1895.
PS
PDF
 Millennial Perspectives in Computer Science,
(jointly edited with J. Davies and J. Woodcock), Palgrave 2000.
 The successes and failures of behavioural models
(with R. Forster and G.M. Reed),
in Millennial Perspectives in Computer Science, Palgrave 2000.
PS
PDF
 The Modelling and Analysis of Security Protocols,
(with P. Ryan, S. Schneider, M. Goldsmith, G. Lowe)
AddisonWesley, 2001.
 On Model Checking Dataindependent Systems with Arrays without Reset
(abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of VCL 2001.
PS
 What can you Decide about Resetable Arrays? , (with R. S. Lazic),
Proceedings of VCL 2001. PS
 Compiling Shared Variable Programs into CSP, Proceedings of PROGRESS
workshop 2001. PS
 Internalising Agents in CSP Protocol Models (Extended Abstract),
(with P. J. Broadfoot) Proceedings of WITS 2002, Portland
PS
 Capturing parallel attacks within the data independence framework,
(with P. J. Broadfoot) Proceedings of CSFW 15 (IEEE Press, 2002)
PS
 On Model Checking Dataindependent Systems with Arrays without Reset,
(with R. S. Lazic and T. C. Newcomb), Theory and Practice of Logic Programming 4
(5 & 6), 659693, 2004. PS
PDF
 Embedding agents within the intruder to detect parallel attacks,
(with P.J. Broadfoot) the Journal of Computer Security, vol 12 (34),
379408, 2004.
PS
PDF
 Authentication in pervasive computing,
(with S.J. Creese, M.H. Goldsmith and I.Zakiuddin), Proceedings of
First International Conference on Pervasive Computing (March 2003), LNCS.
PS
 Bisimulation and refinement reconciled,
(with C.A.R. Hoare, C. Fournet, P.H.B. Gardiner,
R. Milner, S.Rajamani and J. Rehof), Microsoft Technical Report, 2003.
 On the expressive power of CSP refinement,
Preliminary version in Proceedings of AVoCS03,
Southampton University Technical Report, April 2003,
Formal Aspects of Computing, 17 (2), 93112.
PDF
PS
 Polymorphic systems with arrays: decidability and undecidability
(Extended abstract), (with R. S. Lazic and T. C. Newcomb),
Proceedings of SouthEast Europe Workshop on Formal Methods,
August 2003. PDF
 Watchdog transformations for propertyoriented model checking
(with M.H. Goldsmith, N.Moffat, T. Whitworth and I. Zakiuddin), in
Proceedings of FME 2003.
PDF
 The attacker in ubiquitous computing environments:
formalising the threat model, (with S.J. Creese, M.H. Goldsmith
and I.Zakiuddin), Proceedings of FAST 2003, Pisa.
PDF
 Translating CSP trace refinement to UNITY unreachability :
a study in data independence
(with Xu Wang and R.S. Lazic), OUCL Research Report RR0308, April 2003.
PS
 Compiling Statemate Statecharts into CSP and verifying them using FDR
Extended Abstract January 2003
PS
 Seeing beyond divergence June 22, 2004.
Communicating Sequential Processes, the first 25 years,
Springer LNCS 3525,2005..
PS
PDF
 Finitary refinement checks for infinitary specifications
June 2004. Proceedings of CPA 2004.
PDF
 Research directions for trust and security in humancentric computing,
(with Sadie Creese, Michael Goldsmith and Irfan Zakiuddin) Proceedings of SPPC 2004.
PDF
 Responsiveness of Interoperating Components, (with J. N. Reed
and J. E. Sinclair) in FAC vol 16, pp 394411 (2004).
PS
PDF
 Relating Data Independent Trace Checks in CSP with UNITY
Reachability under a Normality Assumption, (with Xu Wang and R. S. Lazic),
Proceedings of IFM 2004, Springer LNCS 2999 (2004).
PDF
 Web Services Security: a preliminary study using Casper and FDR,
(with E. Kleiner) In Proceedings of Automated Reasoning for Security Protocol Analysis (ARSPA 04), Cork, Ireland.
PS PDF
 Polymorphic Systems with Arrays, 2Counter Machines and
Multiset Rewriting, (with R. S. Lazic and Tom Newcomb) Proceedings of INFINITY 2004.
PS PDF
 On Model checking dataindependent systems with arrays with
wholearray operations, (with R. S. Lazic and Tom Newcomb) Communicating Sequential Processes Springer LNCS 3525,2005
PDF
 Exploiting Empirical Engagement in Authentication Protocol Design,
(with Sadie Creese, Michael Goldsmith, Richard Harrison, Paul Whittaker and Irfan Zakiuddin) Proceedings of SPPC 2005
PDF
 On the relationship between Web Services Security and traditional
protocols, (with Eldar Kleiner) to appear in the Proceedings of MFPS 2005
PS PDF
 Revivals,stuckness and the hierarchy of CSP Models, December 2007 (revision of 2005 draft)
PDF
 The pursuit of buffer tolerance, May 2005, unpublished draft
PS PDF
 Confluence thanks to extensional determinism, May 2005,
In Proceedings of Bertinoro meeting on Concurrency, BRICS 2005. Revised version, publication reference ENTCS 1336, 2006
PDF
 Security and trust for ubiquitous communication,
(with Sadie Creese, Mike Reed and Jeff Sanders) prepared for the ITU WSIS Thematic Meeting on Cybersecurity, Geneva, Switzerland June 2005
PDF
 MachineVerifiable Responsiveness,
(with J. N Reed and J. E Sinclair) Proceedings of AVOCS 2005
PDF
 Extending noninterference properties to the timed world,
(with Jian Huang) To appear in the proceedings of SAC 2006
PDF
 Bootstrapping MultiParty AdHoc Security,
(with S. J. Creese, M. H. Goldsmith and Ming Xiao) To appear in the proceedings of SAC 2006,
PDF
 A taxonomy of web services in CSP, (with A. Martin and L. Momtahan)
Proceedings of Web Languages and Formal Methods 2005
PDF
 Humancentred computer security, Unpublished draft
PDF
 Modelling unbounded parallel sessions of security protocols in CSP with E. Kleiner
PDF
 Verifying Statemate Statecharts Using CSP and FDR with Zhenzhong Wu. To appear in the proceedings of ICFEM 2006
PDF and scripts
PDF
PDF
 Efficient group authentication protocols based on human interaction. Proceedings of ARSPA 2006 (with L. H. Nguyen)
PDF
 Responsiveness and stable revivals. (with J. N. Reed and J. E. Sinclair) In Formal Aspects of Computing
Volume 19, Number 3, August 2007 PDF
 Nets with Tokens Which Carry Data. (with Ranko Lazic, Tom Newcomb, Joel Ouaknine and James Worrell)
LNCS 3349 2007 PDF
 SVA, a tool for analysing sharedvariable programms. (with David Hopkins) To appear in the proceedings
of AVoCS 2007 pages 177  183 PDF
 Authenticating ad hoc networks by comparison of short digests. (with L. H. Nguyen) To appear in Information and Computation
PDF
For copies of papers marked HC please contact
elizabeth.walsh@comlab.ox.ac.uk or
sue.taylor@comlab.ox.ac.uk
with address details and a copy will be posted to you.

