Publications:

1. A theory of communicating sequential processes, Oxford University Computing Laboratory technical monograph PRG-16, May 1981 (with S.D. Brookes and C. A. R. Hoare) PDF

2. 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.

3. Criteria for metrisability, Proc. Amer. Math. Soc. 90 (April 1984), 631-640 (with P.J. Collins) http

4. A theory of communicating sequential processes, Journal of the ACM 31, No. 3 (July 1984), 560-599 (with S.D. Brookes and C.A.R. Hoare) PDF

5. Programs as executable predicates, Proceedings of FGCS84 (ICOT, editors) 220-228 (with C.A.R. Hoare). PDF

6. Continuous analogues of axiomatised digital surfaces, Computer Vision, Graphics and Image Processing 29 (January 1985), 60-86 (with T.Y. Kong). PDF

7. A lattice of conditions on topological spaces, Proc. Amer. Math. Soc. 94 (July 1985), 487-496 (with P.J. Collins, G.M. Reed and M.E. Rudin) http

8. Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985) (co-editor with S.D. Brookes and G. Winskel). http

9. An improved failures model for communicating processes, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 281-305 (with S.D. Brookes). PDF

10. Denotational semantics for occam, in Proceedings of the Pittsburgh seminar on concurrency, Springer LNCS 197 (1985), 306-329. PDF

11. 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, 305-324 (with S.D. Brookes).

12. Characterisations of simply-connected finite polyhedra in 3-space, Bull. London Math. Soc. 17 (November 1985), 575-578 (with T.Y. Kong). PDF

13. A theory of binary digital pictures, Computer Vision, Graphics and Image Processing 32 (November 1985), 221-243 (with T.Y. Kong). PDF

14. 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), 103-109. PDF

15. A CSP solution to the ``trains'' problem, in The Analysis of Concurrent Systems (ed. B.T. Denvir et al), Springer LNCS 207 (1985), 384-388. PDF

16. Local symmetry and triangle laws are sufficient for metrisability, Colloquia Mathematica Societatis Janos Bolyai 41, 177-181 (with P.J. Collins). PDF

17. A timed model for communicating sequential processes, Proc.ICALP 86, Springer LNCS 226 (1986), 314-323 (with G.M. Reed).PDF

18. The pursuit of deadlock freedom, Information and Computation 75, 3 (December 1987), 289-327 (with Naiem Dathi). PS

19. Metric spaces as models for real-time 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), 331-343 (with G.M. Reed).PDF

20. Laws of programming, Communications of the ACM 30, 8 (August 1987), 672-686 (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 PRG-42.) PDF

21. 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, (14-16 September 1987, Grenoble, France), IOS B.V., Amsterdam. PS

22. Transforming occam programs, in The Design and Application of Parallel Digital Processors (IEE Conference Publication 298) (1988) (with M.H. Goldsmith). PDF

23. A timed model for communicating sequential processes, Theoretical Computer Science 58 (1988), 249-261 (with G.M. Reed). PDF

24. The laws of occam programming, Theoretical Computer Science 60 (1988), 177-229 (with C.A.R. Hoare). (Previously appeared as Oxford University Computing Laboratory Technical Report PRG-53, 1986.) PDF

25. The decomposition of a rectangle into rectangles of minimal perimeter, University of Maryland Center for Automation Research CAR-TR-169 (1986) (with T.Y. Kong and D.M. Mount) (Also SIAM Journal of Computing 17, 6 pp1215-1231.) PDF

26. An Operational Semantics for CSP (with S. D. Brookes and D. J. Walker) Technical Report 1986 PS

27. An alternative order for the failures model, in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory, July 1988. Also appeared in Journal of Logic and Computation 2, 5 pp557-577. PS

28. Unbounded nondeterminism in CSP, in `Two papers on CSP', technical monograph PRG-67, Oxford University Computing Laboratory, July 1988. Also Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993). PS

29. Unbounded nondeterminism in CSP (with G.Barrett), in the Proceedings of MFPS89 (Springer LNCS 298). PS PDF

30. Deadlock analysis in networks of communicating processes (with S.D. Brookes) Distributed Computing (1991) 4 209-230. PDF

31. A lattice of conditions on topological spaces II (with P. Moody, G.M. Reed and P.J. Collins) Fundamenta Mathematicae 138 (1991) pp69-81 PDF

32. The point-countable 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

33. Maintaining consistency in distributed databases, Technical Monograph PRG-87, Oxford University Computing Laboratory (1990). PS

34. 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.

35. 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.

36. Topology, computer science and the mathematics of convergence, in Topology and Category Theory in Computer Science (Reed, Roscoe, Wachter, eds) OUP 1991. PS

37. Topology and category theory in computer science, (co-edited with G.M. Reed and R.F. Wachter) OUP 1991, (proceedings of a special session at the 1989 Oxford Topology Conference).

38. Analysing TM_FS: a study of nondeterminism in real-time concurrency (with G.M. Reed), in Concurrency: Theory Language and Architecture, (Yonezawa and Ito, eds) Springer LNCS 491. PS

39. CSP and timewise refinement (with G. M. Reed and S. A. Schneider), Proceedings of the BCS-FACS Refinement Workshop (Cambridge, 1991), LNCS.

40. Star covering properties (with E.K. van Douwen, G.M. Reed and I.J. Tree) Topology and its Applications 39 (1991) 71-103. PDF

41. 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).

42. Concepts of digital topology (with T.Y. Kong) Topology and its applications 46 (1992) 219-262. PDF

43. 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).

44. Acyclic monotone normality (with P. Moody), Topology and its Applications 47 (1992) 53-67. PDF

45. Occam in the specification and verification of microprocessors Phil Trans R. Soc. Lond A (1992) 339, 137-151. Also in Mechanised Reasoning and Hardware Design, M.J.C. Gordon and C.A.R. Hoare, eds (Prentice-Hall, 1992). Original paper http Extended Version PS

46. A semantic model for occam II (with M.H. Goldsmith and B.G.O. Scott) Proceedings of Transputing 93.

47. Denotational semantics for occam II (with M.H. Goldsmith and B.G.O. Scott) Oxford University Computing Laboratory Technical monograph PRG-108 (1993). PDF

48. Developing and verifying protocols in CSP, Proceedings of Mierlo workshop on protocols, published by TU Eindhoven.

49. Fixed points without completeness (with M.W. Mislove and S.A. Schneider), Theoretical Computer Science 138, 2 pp273-314.

50. Model-checking CSP, In A Classical Mind: essays in Honour of C.A.R. Hoare, Prentice-Hall 1994. PS

51. A Classical Mind: essays in Honour of C.A.R. Hoare, Prentice-Hall 1994 (editor).

52. Denotational semantics for occam2, Part 1 ( with M.H. Goldsmith and B.G.O. Scott) Transputer Communications 1, 2 pp65-91.

53. Denotational semantics for occam2, Part 2 (with M.H. Goldsmith and B.G.O. Scott) Transputer Communications 2. 1 pp25-67.

54. Non-interference through determinism (with J.C.P. Woodcock and L Wulf) in proceedings of ESORICS 94 (LNCS 875).PDF

55. Non-interference through determinism (with J.C.P. Woodcock and L Wulf) (revised version of above) Journal of Computer Security 4, 1 (pp27--54), 1996. PDF

56. CSP and determinism in security modelling Proceedings of 1995 IEEE Symposium on Security and Privacy (IEEE Computer Society Press) PS

57. Composing and decomposing systems under security properties (with L. Wulf) Proceedings of 1995 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS

58. Modelling and verifying key-exchange protocols using CSP and FDR Proceedings of 1995 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS

59. Hierarchical compression for model-checking CSP, or How to check 10²⁰ 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

60. The timed failures-stability model for Timed CSP (with G.M. Reed) Oxford University Computing Laboratory Technical Monograph PRG-119 (1996)`, also appeared in Theoretical Computer Science, Vol 211 (1999). PS PDF

61. Intensional specifications of security protocols Proceedings of 1996 IEEE Computer Security Foundations Workshop (IEEE Computer Society Press) PS

62. On transition systems and non-well-founded sets, (with R.S. Lazic) Annals of the New York Academiy of Sciences Vol 806, 1996. PS PDF

63. The perfect spy for model-checking crypto-protocols, (with M.H. Goldsmith)} Proceedings of DIMACS workshop on the design and formal verification of crypto-protocols, 1997. (http://dimacs.rutgers.edu/workshops/program2/program.html) PDF

64. 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

65. 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

66. 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 TR-2-98. PS

    (66a) Extended Abstract as above ps file

67. Proving security protocols with model checkers by data independence techniques Proceedings of CSFW 1998, IEEE Press. PS PDF

68. The theory and practice of concurrency, Prentice Hall, 1998, ISBN 0-13-6774409-5, pp. xv+565.amended 2005 PS PDF

69. What is intransitive noninterference? Proceedings of CSFW 1999, IEEE Press. (with M.H. Goldsmith) PS

70. Proving security protocols with model checkers by data independence techniques, (with P.J. Broadfoot) Journal of Computer Security Vol 7 (1999) PS PDF

71. 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

72. 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 5-8 1999, Beijing, China. Published by Kluwer Academic Publishers. PS PDF

73. 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

74. TTP: A case study in combining induction and data independence, (with S.J. Creese) Oxford University Computing Laboratory Technical Report, PRG-TR-1-99. PS

75. Data independent induction over structured networks, (with S.J. Creese) Proceedings of PDPTA2000 PS

76. Automating Data Independence, (with P.J. Broadfoot and G. Lowe) Proceedings of ESORICS2000, LNCS 1895. PS PDF

77. Millennial Perspectives in Computer Science, (jointly edited with J. Davies and J. Woodcock), Palgrave 2000.

78. The successes and failures of behavioural models (with R. Forster and G.M. Reed), in Millennial Perspectives in Computer Science, Palgrave 2000. PS PDF

79. The Modelling and Analysis of Security Protocols, (with P. Ryan, S. Schneider, M. Goldsmith, G. Lowe) Addison-Wesley, 2001.

80. On Model Checking Data-independent Systems with Arrays without Reset (abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of VCL 2001. PS

81. What can you Decide about Resetable Arrays? , (with R. S. Lazic), Proceedings of VCL 2001. PS

82. Compiling Shared Variable Programs into CSP, Proceedings of PROGRESS workshop 2001. PS

83. Internalising Agents in CSP Protocol Models (Extended Abstract), (with P. J. Broadfoot) Proceedings of WITS 2002, Portland PS

84. Capturing parallel attacks within the data independence framework, (with P. J. Broadfoot) Proceedings of CSFW 15 (IEEE Press, 2002) PS

85. On Model Checking Data-independent Systems with Arrays without Reset, (with R. S. Lazic and T. C. Newcomb), Theory and Practice of Logic Programming 4 (5 & 6), 659-693, 2004. PS PDF

86. Embedding agents within the intruder to detect parallel attacks, (with P.J. Broadfoot) the Journal of Computer Security, vol 12 (3-4), 379-408, 2004. PS PDF

87. 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

88. 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.

89. 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), 93-112. PDF PS

90. Polymorphic systems with arrays: decidability and undecidability (Extended abstract), (with R. S. Lazic and T. C. Newcomb), Proceedings of South-East Europe Workshop on Formal Methods, August 2003. PDF

91. Watchdog transformations for property-oriented model checking (with M.H. Goldsmith, N.Moffat, T. Whitworth and I. Zakiuddin), in Proceedings of FME 2003. PDF

92. 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

93. Translating CSP trace refinement to UNITY unreachability : a study in data independence (with Xu Wang and R.S. Lazic), OUCL Research Report RR-03-08, April 2003. PS

94. Compiling Statemate Statecharts into CSP and verifying them using FDR Extended Abstract January 2003 PS

95. Seeing beyond divergence June 22, 2004. Communicating Sequential Processes, the first 25 years, Springer LNCS 3525,2005.. PS PDF

96. Finitary refinement checks for infinitary specifications June 2004. Proceedings of CPA 2004. PDF

97. Research directions for trust and security in human-centric computing, (with Sadie Creese, Michael Goldsmith and Irfan Zakiuddin) Proceedings of SPPC 2004. PDF

98. Responsiveness of Interoperating Components, (with J. N. Reed and J. E. Sinclair) in FAC vol 16, pp 394-411 (2004). PS PDF

99. 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

100. 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

101. Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting, (with R. S. Lazic and Tom Newcomb) Proceedings of INFINITY 2004. PS PDF

102. On Model checking data-independent systems with arrays with whole-array operations, (with R. S. Lazic and Tom Newcomb) Communicating Sequential Processes Springer LNCS 3525,2005 PDF

103. Exploiting Empirical Engagement in Authentication Protocol Design, (with Sadie Creese, Michael Goldsmith, Richard Harrison, Paul Whittaker and Irfan Zakiuddin) Proceedings of SPPC 2005 PDF

104. On the relationship between Web Services Security and traditional protocols, (with Eldar Kleiner) to appear in the Proceedings of MFPS 2005 PS PDF

105. Revivals,stuckness and the hierarchy of CSP Models, December 2007 (revision of 2005 draft) PDF

106. The pursuit of buffer tolerance, May 2005, unpublished draft PS PDF

107. Confluence thanks to extensional determinism, May 2005, In Proceedings of Bertinoro meeting on Concurrency, BRICS 2005. Revised version, publication reference ENTCS 1336, 2006 PDF

108. 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

109. Machine-Verifiable Responsiveness, (with J. N Reed and J. E Sinclair) Proceedings of AVOCS 2005 PDF

110. Extending noninterference properties to the timed world, (with Jian Huang) To appear in the proceedings of SAC 2006 PDF

111. Bootstrapping Multi-Party Ad-Hoc Security, (with S. J. Creese, M. H. Goldsmith and Ming Xiao) To appear in the proceedings of SAC 2006, PDF

112. A taxonomy of web services in CSP, (with A. Martin and L. Momtahan) Proceedings of Web Languages and Formal Methods 2005 PDF

113. Human-centred computer security, Unpublished draft PDF

114. Modelling unbounded parallel sessions of security protocols in CSP with E. Kleiner PDF

115. Verifying Statemate Statecharts Using CSP and FDR with Zhenzhong Wu. To appear in the proceedings of ICFEM 2006 PDF and scripts PDF PDF

116. Efficient group authentication protocols based on human interaction. Proceedings of ARSPA 2006 (with L. H. Nguyen) PDF

117. Responsiveness and stable revivals. (with J. N. Reed and J. E. Sinclair) In Formal Aspects of Computing Volume 19, Number 3, August 2007 PDF

118. Nets with Tokens Which Carry Data. (with Ranko Lazic, Tom Newcomb, Joel Ouaknine and James Worrell) LNCS 3349 2007 PDF

119. SVA, a tool for analysing shared-variable programms. (with David Hopkins) To appear in the proceedings of AVoCS 2007 pages 177 - 183 PDF

120. Authenticating ad hoc networks by comparison of short digests. (with L. H. Nguyen) To appear in Information and Computation PDF

elizabeth.walsh@comlab.ox.ac.uk or sue.taylor@comlab.ox.ac.uk

with address details and a copy will be posted to you.