Concurrency: Publications

[1]	Specification of communicating processes: temporal logic versus refusals-based refinement Gavin Lowe Formal Aspects of Computing, 2008. Details \| BibTeX \| Download (pdf)

[2]	A representative function approach to symmetry exploitation for CSP refinement checking N Moffat, M.H. Goldsmith and A.W. Roscoe In Proceedings of IFCEM 2008 2008. Details \| BibTeX \| Download (pdf)

[3]	On the expressiveness of CSP A.W. Roscoe 2008. Draft of October 23, 2008. Details \| BibTeX \| Download (pdf)

[4]	The three Platonic models of divergence-strict CSP A.W. Roscoe In Proceedings of ICTAC '08 2008. Details \| BibTeX \| Download (pdf)

[5]	Revivals,stuckness and the hierarchy of CSP Models A. W. Roscoe December 2008. to appear (revision of 2005 and 2007 drafts). Details \| BibTeX \| Download (pdf)

[6]	Formal verification of not fully symmetric systems using counter abstraction Tomasz Mazur In Proceedings of the MOdelling and VErifying Process (MOVEP'08) 2008. Details \| BibTeX \| Link (pdf)

[7]	Model Checking Concurrent Linux Device Drivers Witkowski, Thomas et al. In 22nd IEEE International Conference on Automated Software Engineering (ASE) pages 501—504. IEEE, 2007. Details \| BibTeX \| Link \| DOI (10.1145/1321631.1321719)

[8]	Static Analysis to Enhance the Power of Model Checking for Concurrent Software Clarke, Edmund, Kroening, Daniel and Reps, Thomas In Department of Defense Sponsored Information Security Research pages 349—360. Wiley. July 2007. Details \| BibTeX

[9]	SVA, a tool for analysing shared-variable programms A. W. Roscoe, David Hopkins In Proceedings of AVoCS 2007 pages 177—183. 2007. to appear. Details \| BibTeX \| Link (pdf)

[10]	Responsiveness and stable revivals A. W. Roscoe, J. N. Reed and J. E. Sinclair Formal Aspects of Computing, Vol. 19, No. 3, August 2007. Details \| BibTeX \| Link (pdf)

[11]	Nets with Tokens Which Carry Data A. W. Roscoe et al. Springer LNCS 3349, 2007. Details \| BibTeX \| Download

[12]	Counter Abstraction in the CSP/FDR setting Tomasz Mazur, Gavin Lowe In Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS'07) 2007. Details \| BibTeX \| Link (pdf)

[13]	On CSP refinement tests that run multiple copies of a process Gavin Lowe 2007. Details \| BibTeX \| Download (pdf)

[14]	Verification of Boolean Programs with Unbounded Thread Creation Cook, Byron, Kroening, Daniel and Sharygina, Natasha Theoretical Computer Science (TCS), Vol. 388, pages 227—242. 2007. Details \| BibTeX

[15]	On Timed Models and Full Abstraction Gavin Lowe, Joël Ouaknine Electr. Notes Theor. Comput. Sci. Vol. 155, pages 497-519. 2006. Details \| BibTeX \| Link (ps) \| DOI (10.1016/j.entcs.2005.11.070)

[16]	Modelling unbounded parallel sessions of security protocols in CSP A. W. Roscoe, E. Kleiner 2006. Details \| BibTeX \| Link (pdf)

[17]

Verifying Statemate Statecharts Using CSP and FDR

A. W. Roscoe, Zhenzhong Wu

In Proceedings of ICFEM 2006 2006.

scripts: http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/115.csp; http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/115statechartcompiler.csp

Details | BibTeX | Link (pdf)

[18]	A hierarchy of failures-based models: theory and application Christie Bolton, Gavin Lowe Theoretical Computer Science, Vol. 330, No. 3, pages 407-438. 2005. Details \| BibTeX \| Link (ps) \| DOI (10.1016/j.tcs.2004.10.004)

[19]	A taxonomy of web services in CSP A. W. Roscoe, A. Martin and L. Momtahan In Proceedings of Web Languages and Formal Methods 2005 2005. Details \| BibTeX \| Link (pdf)

[20]	Confluence thanks to extensional determinism A. W. Roscoe In Proceedings of Bertinoro meeting on Concurrency, BRICS 2005 May 2005. Revised version, publication reference ENTCS 1336, 2006. Details \| BibTeX \| Link (pdf)

[21]	Machine-Verifiable Responsiveness A. W. Roscoe, J. N Reed and J. E Sinclair In Proceedings of AVOCS 2005 2005. Details \| BibTeX \| Link (pdf)

[22]	On Model checking data-independent systems with arrays with whole-array operations A. W. Roscoe, R. S. Lazic and Tom Newcomb In Communicating Sequential Processes No. 3525, Springer LNCS, 2005. Details \| BibTeX \| Link (pdf)

[23]	Seeing beyond divergence A. W. Roscoe In Communicating Sequential Processes, the first 25 years No. 3525, Springer LNCS, 2005. Details \| BibTeX \| Link (pdf)

[24]	The pursuit of buffer tolerance A. W. Roscoe May 2005. unpublished draft. Details \| BibTeX \| Link (pdf)

[25]	A Hierarchy of Failures-Based Models Christie Bolton, Gavin Lowe Electr. Notes Theor. Comput. Sci. Vol. 96, pages 129-152. 2004. Details \| BibTeX \| DOI (10.1016/j.entcs.2004.04.025)

[26]	On the Application of Counterexample-Guided Abstraction refinement and data independence to the parameterised model checking problem Gavin Lowe In Proceedings of the Third International Workshop on Automatic Verification of Infinite-State Systems, (AVIS 2004) 2004. Details \| BibTeX \| Link (ps)

[27]	A taxonomy of web services using CSP Lee Momtahan, Andrew Martin and A. W. Roscoe No. RR-04-22, Technical Report, Oxford University Computing Laboratory. October 2004. Details \| BibTeX \| Download (ps)

[28]	Finitary refinement checks for infinitary specifications A. W. Roscoe In Proceedings of CPA 2004 June 2004. Details \| BibTeX \| Link (pdf)

[29]	Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting A. W. Roscoe, R. S. Lazic and Tom Newcomb In Proceedings of INFINITY 2004 2004. Details \| BibTeX \| Link (pdf)

[30]	Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption A. W. Roscoe, Xu Wang and R. S. Lazic In Proceedings of IFM 2004 Vol. 2999. Springer LNCS, 2004. Details \| BibTeX \| Link (pdf)

[31]	Responsiveness of Interoperating Components A. W. Roscoe, J. N. Reed and J. E. Sinclair Formal Aspects of Computing, Vol. 16, pages 394—411. 2004. Details \| BibTeX \| Link (pdf)

[32]	On Model Checking Data-independent Systems with Arrays without Reset A. W. Roscoe, R. S. Lazic and T. C. Newcomb Theory and Practice of Logic Programming, Vol. 4, No. 5 & 6, pages 659-693. 2004. Details \| BibTeX \| Link (pdf)

[33]	Bisimulation and refinement reconciled A. W. Roscoe et al. Technical Report, Microsoft. 2003. Details \| BibTeX

[34]	Polymorphic systems with arrays: decidability and undecidability A. W. Roscoe, R. S. Lazic and T. C. Newcomb In Proceedings of South-East Europe Workshop on Formal Methods August 2003. Extended abstract. Details \| BibTeX \| Link (pdf)

[35]	Watchdog transformations for property-oriented model checking A. W. Roscoe et al. In Proceedings of FME 2003 2003. Details \| BibTeX \| Link (pdf)

[36]	Compiling Statemate Statecharts into CSP and verifying them using FDR A. W. Roscoe January 2003. Extended Abstract. Details \| BibTeX \| Link (ps)

[37]	Translating CSP trace refinement to UNITY unreachability : a study in data independence A. W. Roscoe, Xu Wang and R.S. Lazic No. RR-03-08, Technical Report, Oxford University Computing Laboratory. 2003. Details \| BibTeX \| Download (ps.gz)

[38]	On the expressive power of CSP refinement A. W. Roscoe Formal Aspects of Computing, Vol. 17 of 2, pages 93—112. 2003. Preliminary version in Proceedings of AVoCS03, Southampton University Technical Report, April 2003. Details \| BibTeX \| Link (ps)

[39]	Capturing parallel attacks within the data independence framework A. W. Roscoe, P. J. Broadfoot In Proceedings of CSFW 15 IEEE Press, 2002. Details \| BibTeX \| Link (ps)

[40]	Internalising Agents in CSP Protocol Models A. W. Roscoe, P. J. Broadfoot In Proceedings of WITS 2002 2002. Extended Abstract. Details \| BibTeX \| Link (ps)

[41]	On Model Checking Data-independent Systems with Arrays without Reset A. W. Roscoe, R. S. Lazic and T. C. Newcomb In Proceedings of VCL 2001 2001. Details \| BibTeX \| Link (ps)

[42]	What can you Decide about Resetable Arrays? A. W. Roscoe, R. S. Lazic In Proceedings of VCL 2001 2001. Details \| BibTeX \| Link (ps)

[43]	Compiling Shared Variable Programs into CSP A. W. Roscoe In Proceedings of PROGRESS workshop 2001 2001. Details \| BibTeX \| Link (ps)

[44]

Automating Data Independence

Philippa J. Broadfoot, Gavin Lowe and A. W. Roscoe

In Frédéric Cuppens et al. , editors, Computer Security - ESORICS 2000, 6th European Symposium on Research in Computer Security, Toulouse, France, October 4-6, 2000, Proceedings Vol. 1895 of Lecture Notes in Computer Science, pages 175-190. Springer, 2000.

Details | BibTeX | Link (ps) | DOI (10.1007/10722599_11)

[45]	Automating Data Independence A. W. Roscoe, P.J. Broadfoot and G. Lowe In Proceedings of ESORICS2000 Vol. 1895. LNCS, 2000. Details \| BibTeX \| Link (pdf)

[46]	Data independent induction over structured networks A. W. Roscoe, S.J. Creese In Proceedings of PDPTA2000 2000. Details \| BibTeX \| Link (ps)

[47]	The successes and failures of behavioural models A. W. Roscoe, R. Forster and G.M. Reed In Millennial Perspectives in Computer Science Palgrave. 2000. Details \| BibTeX \| Link (pdf)

[48]	Data independence with predicate symbols A. W. Roscoe, R.S. Lazic In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99) Vol. I. CSREA Press, 1999. Details \| BibTeX \| Link (ps)

[49]	Formal Verification of Arbitrary Network Topologies A. W. Roscoe, S.J. Creese In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99) Vol. II. CSREA Press, 1999. Details \| BibTeX \| Link (pdf)

[50]	TTP: A case study in combining induction and data independence A. W. Roscoe, S.J. Creese No. {PRG-TR-1-99}, Technical Report, Oxford University Computing Laboratory. 1999. Details \| BibTeX \| Link (ps)

[51]	Proving security protocols with model checkers by data independence techniques A. W. Roscoe, P.J. Broadfoot Journal of Computer Security, Vol. 7. 1999. Details \| BibTeX \| Link (pdf)

[52]	Proving security protocols with model checkers by data independence techniques A. W. Roscoe In Proceedings of CSFW 1998 IEEE Press, 1998. Details \| BibTeX \| Link (pdf)

[53]	The theory and practice of concurrency A. W. Roscoe Prentice Hall. 1998. Details \| BibTeX \| Link (pdf)

[54]	Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays A. W. Roscoe, R. Lazic In Proceedings of INFINITY'98 July 1998. extended version as Oxford University Computing Laboratory TR-2-98. Details \| BibTeX \| Link (ps)

[55]	A Case Study of the Formal Specification of a Parallel System using CSP A. W. Roscoe, S. Kiyamura In S. Noguchi, M. Ota, editors, Correct Models of Parallel Computing IOS Press. 1997. Details \| BibTeX

[56]	The timed failures-stability model for Timed CSP A. W. Roscoe, G.M. Reed No. {PRG-119}, Technical Report, Oxford University Computing Laboratory. 1996. also appeared in Theoretical Computer Science, Vol 211 (1999). Details \| BibTeX \| Link (pdf)

[57]	Probabilistic and Prioritized Models of Timed CSP Gavin Lowe Theor. Comput. Sci. Vol. 138, No. 2, pages 315-352. 1995. Details \| BibTeX \| Link (ps.gz) \| DOI (10.1016/0304-3975(94)00171-E)

[58]	Scheduling-Oriented Models for Real-Time Systems Gavin Lowe The Computer Journal, Vol. 38, No. 6, pages 443-456. 1995. Details \| BibTeX \| Link (ps.gz)

[59]	Refinement of Complex Systems: A Case Study Gavin Lowe, Hussein Zedan The Computer Journal, Vol. 38, No. 10, pages 785-800. 1995. Details \| BibTeX \| Link (ps.gz)

[60]

Hierarchical compression for model-checking CSP, or How to check 10^20 dining philosophers for deadlock

A. W. Roscoe, P.H.B. Gardiner, M.H. Goldsmith, J.R. Hulance, D.M.Jackson and J.B. Scattergood

In Proceedings of TACAS 1995 BRICS, 1995.

also revised in a version of these proceedings published by LNCS.

Details | BibTeX | Link (pdf)

[61]	Denotational semantics for occam2, Part 2 A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott Transputer Communications, Vol. 2 of 1, pages 25—67. 1994. Details \| BibTeX

[62]	Denotational semantics for occam2, Part 1 A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott Transputer Communications, Vol. 1 of 2, pages 65—91. 1994. Details \| BibTeX

[63]	A Classical Mind: essays in Honour of C.A.R. Hoare A. W. Roscoe, editor Prentice-Hall. 1994. Details \| BibTeX

[64]	Model-checking CSP A. W. Roscoe In A Classical Mind: essays in Honour of C.A.R. Hoare chapter 21, Prentice-Hall. 1994. Details \| BibTeX \| Link (ps)

[65]	Probabilities and Priorities in Timed CSP Gavin Lowe PhD Thesis, DPhil thesis. Oxford University Computing Laboratory. 1993. Details \| BibTeX \| Link (ps.gz)

[66]	Denotational semantics for occam II A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott No. PRG-108, Technical Report, Oxford University Computing Laboratory. 1993. Details \| BibTeX \| Link (pdf)

[67]	Developing and verifying protocols in CSP A. W. Roscoe In Proceedings of Mierlo workshop on protocols TU Eindhoven, 1993. Details \| BibTeX

[68]

Occam in the specification and verification of microprocessors

A. W. Roscoe

Phil Trans R. Soc. Lond A, Vol. 339, pages 137-151. 1992.

Also in Mechanised Reasoning and Hardware Design, M.J.C. Gordon and C.A.R. Hoare, eds (Prentice-Hall, 1992), extended version available at http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/45ex.ps

Details | BibTeX | Link

[69]	Timed CSP: theory and practice A. W. Roscoe et al. In Proceedings of REX Workshop Vol. 600. LNCS, 1992. Details \| BibTeX

[70]	Analysing TM_FS: a study of nondeterminism in real-time concurrency A. W. Roscoe, G.M. Reed Concurrency: Theory Language and Architecture, Vol. 491. 1991. Details \| BibTeX \| Link (ps)

[71]	A semantic model for occam II A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott Proceedings of Transputing, Vol. 93. 1991. Details \| BibTeX

[72]	Deadlock analysis in networks of communicating processes A. W. Roscoe, S.D. Brookes Distributed Computing, No. 4, pages 209—230. 1991. Details \| BibTeX \| Link (pdf)

[73]	CSP and timewise refinement A. W. Roscoe, G. M. Reed and S. A. Schneider In Proceedings of the BCS-FACS Refinement Workshop LNCS, 1991. Details \| BibTeX

[74]	Maintaining consistency in distributed databases A. W. Roscoe No. {PRG-87}, Technical Report, Oxford University Computing Laboratory. 1990. Details \| BibTeX \| Link (ps)

[75]	Communication and correctness in Timed CSP A. W. Roscoe et al. Technical Report, Esprit SPEC project. 1990. Details \| BibTeX

[76]	A temporal logic for Timed CSP D.M. Jackson et al. Technical Report, Esprit SPEC project. 1990. Details \| BibTeX

[77]	Unbounded nondeterminism in CSP A. W. Roscoe, G.Barrett In Proceedings of MFPS89 No. 298, Springer, 1989. Details \| BibTeX \| Link (pdf)

[78]	A timed model for communicating sequential processes A. W. Roscoe, G.M. Reed Theoretical Computer Science, Vol. 58, pages 249—261. 1988. Details \| BibTeX \| Link (pdf)

[79]	The laws of occam programming A. W. Roscoe, C.A.R. Hoare Theoretical Computer Science, Vol. 60, pages 177—229. 1988. Previously appeared as Oxford University Computing Laboratory Technical Report PRG-53, 1986. Details \| BibTeX \| Link (pdf)

[80]	Unbounded nondeterminism in CSP A. W. Roscoe No. PRG-67, Technical Report, Oxford University Computing Laboratory. July 1988. in Two papers on CSP, Also appeared in Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993). Details \| BibTeX \| Link (ps)

[81]	Transforming occam programs A. W. Roscoe, M.H. Goldsmith In The Design and Application of Parallel Digital Processors No. 298, 1988. Details \| BibTeX \| Link (pdf)

[82]	Metric spaces as models for real-time concurrency A. W. Roscoe, G.M. Reed In Main et al, editor, Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans, 1987) No. 298, pages 331—343. Springer, 1988. Details \| BibTeX \| Link (pdf)

[83]	An alternative order for the failures model A. W. Roscoe No. PRG-67, Technical Report, Oxford University Computing Laboratory. July 1988. in Two papers on CSP, Also appeared in Journal of Logic and Computation 2, 5 pp557-577. Details \| BibTeX \| Link (ps)

[84]	The pursuit of deadlock freedom A. W. Roscoe, Naiem Dathi Information and Computation, Vol. 75, No. 3, pages 289—327. December 1987. Details \| BibTeX \| Link (ps)

[85]	Routing messages through networks: an exercise in deadlock avoidance A. W. Roscoe In Muntean et al., editor, Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting Amsterdam. 1987. IOS B.V. Details \| BibTeX \| Link (ps)

[86]	An Operational Semantics for CSP A. W. Roscoe, S. D. Brookes and D. J. Walker Technical Report, Oxford University Computing Laboratory. 1986. Details \| BibTeX \| Link (ps)

[87]	A timed model for communicating sequential processes A. W. Roscoe, G.M. Reed In Proc.ICALP 86 No. 226, pages 314—323. Springer, 1986. Details \| BibTeX \| Link (pdf)

[88]	Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification A. W. Roscoe In B.T. Denvir et al, editor, The Analysis of Concurrent Systems No. 207, pages 103—109. Springer, 1985. Details \| BibTeX \| Link (pdf)

[89]	Proceedings of the Pittsburgh seminar on concurrency A. W. Roscoe, S.D. Brookes and G. Winskel, editors No. 197, Springer. 1985. Details \| BibTeX \| Link

[90]	Denotational semantics for occam A. W. Roscoe In Proceedings of the Pittsburgh seminar on concurrency No. 197, pages 306—329. Springer, 1985. Details \| BibTeX \| Link (pdf)

[91]	Deadlock analysis in networks of communicating processes A. W. Roscoe, S.D. Brookes In K.R. Apt, editor, Logics and Models of Concurrent Systems Vol. 13 of NATO ASI series F, pages 305—324. Springer, 1985. Details \| BibTeX

[92]	An improved failures model for communicating processes A. W. Roscoe, S.D. Brookes In Proceedings of the Pittsburgh seminar on concurrency No. 197, pages 281—305. Springer, 1985. Details \| BibTeX \| Link (pdf)

[93]	A CSP solution to the trains problem A. W. Roscoe In B.T. Denvir et al, editor, The Analysis of Concurrent Systems No. 207, pages 384—388. Springer, 1985. Details \| BibTeX \| Link (pdf)

[94]	A theory of communicating sequential processes A. W. Roscoe, S.D. Brookes and C.A.R. Hoare Journal of the ACM, No. 3, pages 560—599. July 1984. Details \| BibTeX \| Link (pdf)

[95]	Programs as executable predicates A. W. Roscoe, C.A.R. Hoare In Proceedings of FGCS84 (ICOT, editors) pages 220—228. 1984. Details \| BibTeX \| Link (pdf)

[96]	A mathematical theory of communicating processes A. W. Roscoe PhD Thesis, D. Phil. thesis. Oxford University. 1982. Please note this is a 270 page, 118 Mb scanned file and will take some time to download. Details \| BibTeX \| Link (pdf)

[97]	A theory of communicating sequential processes A. W. Roscoe, S.D. Brookes and C. A. R. Hoare No. {PRG-16}, Technical Report, Oxford University Computing Laboratory. May 1981. Details \| BibTeX \| Link (pdf)