@inproceedings{Bate13,
  title = "{Scalable Performance for Scala Message-Passing Concurrency}",
  author = "Bate, Andrew",
  year = "2013",
  booktitle = "{Communicating Process Architectures 2013}",
  editor = "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan B{\ae}kgaard and Sampson, Adam T.",
  isbn = "978-0-9565409-7-3",
  month = "nov",
  pages = "113--132",
}
@inproceedings{BateLowe12,
  title = "{A Debugger for Communicating Scala Objects}",
  author = "Andrew Bate and Gavin Lowe",
  year = "2012",
  booktitle = "{Communicating Process Architectures 2012}",
  editor = "Welch, Peter H. and Barnes, Frederick R. M. and Chalmers, Kevin and Pedersen, Jan B{\ae}kgaard and Sampson, Adam T.",
  isbn = "978-0-9565409-5-9",
  month = "aug",
  pages = "135--154",
}
@article{exprcsp,
  title = "On the expressiveness of CSP",
  author = "A.W. Roscoe",
  year = "2011",
  note = "Draft of February 2011, which is very different from previous draft (2008).",
}
@article{temporal-logic,
  title = "Specification of communicating processes: temporal logic versus refusals-based refinement",
  author = "Gavin Lowe",
  year = "2008",
  journal = "Formal Aspects of Computing",
}
@inproceedings{sym08,
  title = "A representative function approach to symmetry exploitation for CSP refinement checking",
  author = "N Moffat and M.H. Goldsmith and A.W. Roscoe",
  year = "2008",
  booktitle = "Proceedings of IFCEM 2008",
}
@inproceedings{biro121,
  title = "The three Platonic models of divergence-strict CSP",
  author = "A.W. Roscoe",
  year = "2008",
  booktitle = "Proceedings of ICTAC '08",
}
@unpublished{Revivals,
  title = "{Revivals,stuckness and the hierarchy of CSP Models}",
  author = "A. W. Roscoe",
  year = "2008",
  journal = "JLAP",
  month = "December",
  note = "to appear (revision of 2005 and 2007 drafts)",
}
@inproceedings{mazur:2008,
  title = "Formal verification of not fully symmetric systems using counter abstraction",
  author = "Tomasz Mazur",
  year = "2008",
  booktitle = "Proceedings of the MOdelling and VErifying Process (MOVEP'08)",
  url = "http://web.comlab.ox.ac.uk/people/tomasz.mazur/publications/tomasz_mazur-movep08-phd.pdf",
}
@inproceedings{wbwk2007,
  title = "Model Checking Concurrent {Linux} Device Drivers",
  author = "Witkowski, Thomas and Blanc, Nicolas and Weissenbacher, Georg and Kroening, Daniel",
  year = "2007",
  booktitle = "22nd IEEE International Conference on Automated Software Engineering (ASE)",
  isbn = "978-1-59593-882-4",
  pages = "501--504",
  publisher = "IEEE",
  url = "http://doi.acm.org/10.1145/1321631.1321719",
  doi = "10.1145/1321631.1321719",
}
@incollection{ckr2007,
  title = "Static Analysis to Enhance the Power of Model Checking for Concurrent Software",
  author = "Clarke, Edmund and Kroening, Daniel and Reps, Thomas",
  year = "2007",
  booktitle = "Department of Defense Sponsored Information Security Research",
  isbn = "0-471-78756-6",
  month = "July",
  pages = "349--360",
  publisher = "Wiley",
}
@inproceedings{SVA,
  title = "{SVA, a tool for analysing shared-variable programms}",
  author = "A. W. Roscoe and David Hopkins",
  year = "2007",
  booktitle = "{Proceedings of AVoCS 2007}",
  note = "to appear",
  pages = "177--183",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/119.pdf",
}
@article{StableRevivals,
  title = "Responsiveness and stable revivals",
  author = "A. W. Roscoe and J. N. Reed and J. E. Sinclair",
  year = "2007",
  journal = "{Formal Aspects of Computing}",
  month = "August",
  number = "3",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/117.pdf",
  volume = "19",
}
@article{NetsWithTokens,
  title = "Nets with Tokens Which Carry Data",
  author = "A. W. Roscoe and Ranko Lazic and Tom Newcomb and Joel Ouaknine and James Worrell",
  year = "2007",
  journal = "{Springer LNCS 3349}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/118.pdf",
}
@inproceedings{mazur:2007,
  title = "Counter Abstraction in the CSP/FDR setting",
  author = "Tomasz Mazur and Gavin Lowe",
  year = "2007",
  booktitle = "Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS'07)",
  url = "http://web.comlab.ox.ac.uk/people/tomasz.mazur/publications/counterabstraction_AVoCS.pdf",
}
@conference{harness,
  title = "On CSP refinement tests that run multiple copies of a process",
  author = "Gavin Lowe",
  year = "2007",
  journal = "Proceedings of Workshop on Automated Verification of Critical Systems (AVoCS 2007)",
}
@article{cks2007-tcs,
  title = "Verification of {Boolean} Programs with Unbounded Thread Creation",
  author = "Cook, Byron and Kroening, Daniel and Sharygina, Natasha",
  year = "2007",
  journal = "Theoretical Computer Science (TCS)",
  pages = "227--242",
  publisher = "Elsevier",
  volume = "388",
}
@article{journals/entcs/LoweO06,
  title = "On Timed Models and Full Abstraction",
  author = "Gavin Lowe and Jo{\"e}l Ouaknine",
  year = "2006",
  journal = "Electr. Notes Theor. Comput. Sci.",
  pages = "497-519",
  url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/timedTesting.ps",
  volume = "155",
  doi = "10.1016/j.entcs.2005.11.070",
}
@unpublished{modellingUnbounded,
  title = "Modelling unbounded parallel sessions of security protocols in {CSP}",
  author = "A. W. Roscoe and E. Kleiner",
  year = "2006",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/114.pdf",
}
@inproceedings{VerifyingStalemate,
  title = "{Verifying Statemate Statecharts Using CSP and FDR}",
  author = "A. W. Roscoe and Zhenzhong Wu",
  year = "2006",
  booktitle = "{Proceedings of ICFEM 2006}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/115.pdf",
}
@article{journals/tcs/BoltonL05,
  title = "A hierarchy of failures-based models: theory and application",
  author = "Christie Bolton and Gavin Lowe",
  year = "2005",
  journal = "Theoretical Computer Science",
  number = "3",
  pages = "407-438",
  url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/EXPRESS.ps",
  volume = "330",
  doi = "10.1016/j.tcs.2004.10.004",
}
@inproceedings{WebServiceTaxonomy,
  title = "A taxonomy of web services in {CSP}",
  author = "A. W. Roscoe and A. Martin and L. Momtahan",
  year = "2005",
  booktitle = "{Proceedings of Web Languages and Formal Methods 2005}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/112.pdf",
}
@inproceedings{ConfluenceThanks,
  title = "Confluence thanks to extensional determinism",
  author = "A. W. Roscoe",
  year = "2005",
  booktitle = "{Proceedings of Bertinoro meeting on Concurrency, BRICS 2005}",
  month = "May",
  note = "{Revised version, publication reference ENTCS 1336, 2006}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/107.pdf",
}
@inproceedings{MachineVerifiableResponsiveness,
  title = "Machine-Verifiable Responsiveness",
  author = "A. W. Roscoe and J. N Reed and J. E Sinclair",
  year = "2005",
  booktitle = "{Proceedings of AVOCS 2005}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/109.pdf",
}
@inproceedings{Whole-Array,
  title = "On Model checking data-independent systems with arrays with whole-array operations",
  author = "A. W. Roscoe and R. S. Lazic and Tom Newcomb",
  year = "2005",
  booktitle = "{Communicating Sequential Processes}",
  number = "3525",
  publisher = "Springer {LNCS}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/102.pdf",
}
@inproceedings{SeeingBeyondDivergence,
  title = "Seeing beyond divergence",
  author = "A. W. Roscoe",
  year = "2005",
  booktitle = "{Communicating Sequential Processes, the first 25 years}",
  number = "3525",
  publisher = "{Springer LNCS}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/95.pdf",
}
@unpublished{Pursuit,
  title = "The pursuit of buffer tolerance",
  author = "A. W. Roscoe",
  year = "2005",
  month = "May",
  note = "unpublished draft",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/106.pdf",
}
@article{journals/entcs/BoltonL04,
  title = "A Hierarchy of Failures-Based Models",
  author = "Christie Bolton and Gavin Lowe",
  year = "2004",
  journal = "Electr. Notes Theor. Comput. Sci.",
  pages = "129-152",
  volume = "96",
  doi = "10.1016/j.entcs.2004.04.025",
}
@inproceedings{inproc/avis,
  title = "On the Application of Counterexample-Guided Abstraction refinement and data independence to the parameterised model checking problem",
  author = "Gavin Lowe",
  year = "2004",
  booktitle = "{Proceedings of the Third International Workshop on Automatic Verification of Infinite-State Systems, (AVIS 2004)}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/CEGAR.ps",
}
@techreport{RR-04-22,
  title = "A taxonomy of web services using CSP",
  author = "Lee Momtahan and Andrew Martin and A. W. Roscoe",
  year = "2004",
  institution = "Oxford University Computing Laboratory",
  month = "October",
  number = "RR-04-22",
}
@inproceedings{Finitaryrefinementchecks,
  title = "Finitary refinement checks for infinitary specifications",
  author = "A. W. Roscoe",
  year = "2004",
  booktitle = "{Proceedings of CPA 2004}",
  month = "June",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/96.pdf",
}
@inproceedings{PolymorphicSystemsWithArrays,
  title = "Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting",
  author = "A. W. Roscoe and R. S. Lazic and Tom Newcomb",
  year = "2004",
  booktitle = "{Proceedings of INFINITY 2004}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/101.pdf",
}
@inproceedings{NormalityAssumption,
  title = "{Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption}",
  author = "A. W. Roscoe and Xu Wang and R. S. Lazic",
  year = "2004",
  booktitle = "{Proceedings of IFM 2004}",
  publisher = "{Springer LNCS}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/99.pdf",
  volume = "2999",
}
@article{Responsiveness,
  title = "Responsiveness of Interoperating Components",
  author = "A. W. Roscoe and J. N. Reed and J. E. Sinclair",
  year = "2004",
  journal = "Formal Aspects of Computing",
  pages = "394--411",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/98.pdf",
  volume = "16",
}
@article{ArraysWithoutReset,
  title = "On Model Checking Data-independent Systems with Arrays without Reset",
  author = "A. W. Roscoe and R. S. Lazic and T. C. Newcomb",
  year = "2004",
  journal = "Theory and Practice of Logic Programming",
  number = "5 & 6",
  pages = "659-693",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/85.pdf",
  volume = "4",
}
@techreport{Bisimulation,
  title = "Bisimulation and refinement reconciled",
  author = "A. W. Roscoe and C.A.R. Hoare and C. Fournet and P.H.B. Gardiner and R. Milner and S.Rajamani and J. Rehof",
  year = "2003",
  institution = "Microsoft",
}
@inproceedings{PolymorphicSystems,
  title = "Polymorphic systems with arrays: decidability and undecidability",
  author = "A. W. Roscoe and R. S. Lazic and T. C. Newcomb",
  year = "2003",
  booktitle = "{Proceedings of South-East Europe Workshop on Formal Methods}",
  month = "August",
  note = "Extended abstract",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/90.pdf",
}
@inproceedings{WatchdogTransformations,
  title = "Watchdog transformations for property-oriented model checking",
  author = "A. W. Roscoe and M.H. Goldsmith and N.Moffat and T. Whitworth and I. Zakiuddin",
  year = "2003",
  booktitle = "{Proceedings of FME 2003}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/91.pdf",
}
@unpublished{CompilingStalemateStatecharts,
  title = "{Compiling Statemate Statecharts into CSP and verifying them using FDR}",
  author = "A. W. Roscoe",
  year = "2003",
  month = "January",
  note = "Extended Abstract",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/94ab.ps",
}
@techreport{UNITYunreachability,
  title = "{Translating CSP trace refinement to UNITY unreachability : a study in data independence}",
  author = "A. W. Roscoe and Xu Wang and R.S. Lazic",
  year = "2003",
  institution = "Oxford University Computing Laboratory",
  month = "April",
  number = "RR-03-08",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/93.ps",
}
@article{ExpressivePower,
  title = "{On the expressive power of CSP refinement}",
  author = "A. W. Roscoe",
  year = "2003",
  journal = "{Formal Aspects of Computing}",
  note = "{Preliminary version in Proceedings of AVoCS03, Southampton University Technical Report, April 2003}",
  pages = "93--112",
  series = "2",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/89.ps",
  volume = "17",
}
@inproceedings{CapturingParallelAttacks,
  title = "Capturing parallel attacks within the data independence framework",
  author = "A. W. Roscoe and P. J. Broadfoot",
  year = "2002",
  booktitle = "{Proceedings of CSFW 15}",
  publisher = "{IEEE Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/84.ps",
}
@inproceedings{InternalisingAgents,
  title = "{Internalising Agents in CSP Protocol Models}",
  author = "A. W. Roscoe and P. J. Broadfoot",
  year = "2002",
  booktitle = "{Proceedings of WITS 2002}",
  note = "Extended Abstract",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/83.ps",
}
@inproceedings{WithoutReset,
  title = "On Model Checking Data-independent Systems with Arrays without Reset",
  author = "A. W. Roscoe and R. S. Lazic and T. C. Newcomb",
  year = "2001",
  booktitle = "{Proceedings of VCL 2001}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/80.ps",
}
@inproceedings{WhatCanYouDecide,
  title = "What can you Decide about Resetable Arrays?",
  author = "A. W. Roscoe and R. S. Lazic",
  year = "2001",
  booktitle = "{Proceedings of VCL 2001}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/81.ps",
}
@inproceedings{Compiling,
  title = "{Compiling Shared Variable Programs into CSP}",
  author = "A. W. Roscoe",
  year = "2001",
  booktitle = "{Proceedings of PROGRESS workshop 2001}",
}
@inproceedings{conf/esorics/BroadfootLR00,
  title = "Automating Data Independence",
  author = "Philippa J. Broadfoot and Gavin Lowe and A. W. Roscoe",
  year = "2000",
  booktitle = "Computer Security - ESORICS 2000, 6th European Symposium on Research in Computer Security, Toulouse, France, October 4-6, 2000, Proceedings",
  editor = "Fr{\'e}d{\'e}ric Cuppens and Yves Deswarte and Dieter Gollmann and Michael Waidner",
  isbn = "3-540-41031-7",
  pages = "175-190",
  publisher = "Springer",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/gavin.lowe/Security/Papers/BLR_esorics00.ps",
  volume = "1895",
  doi = "10.1007/10722599_11",
}
@inproceedings{AutomatingDataIndependence,
  title = "Automating Data Independence",
  author = "A. W. Roscoe and P.J. Broadfoot and G. Lowe",
  year = "2000",
  booktitle = "{Proceedings of ESORICS2000}",
  publisher = "LNCS",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/76.pdf",
  volume = "1895",
}
@inproceedings{StructuredNetworks,
  title = "Data independent induction over structured networks",
  author = "A. W. Roscoe and S.J. Creese",
  year = "2000",
  booktitle = "{Proceedings of PDPTA2000}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/75.ps",
}
@inbook{SuccessesAndFailures,
  title = "The successes and failures of behavioural models",
  author = "A. W. Roscoe and R. Forster and G.M. Reed",
  year = "2000",
  booktitle = "Millennial Perspectives in Computer Science",
  publisher = "Palgrave",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/78.pdf",
}
@inproceedings{PredicateSymbols,
  title = "Data independence with predicate symbols",
  author = "A. W. Roscoe and R.S. Lazic",
  year = "1999",
  booktitle = "{Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99)}",
  publisher = "{CSREA Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/71.ps",
  volume = "I",
}
@inproceedings{ArbitraryNetworkTopologies,
  title = "{Formal Verification of Arbitrary Network Topologies}",
  author = "A. W. Roscoe and S.J. Creese",
  year = "1999",
  booktitle = "{Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99)}",
  publisher = "{CSREA Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/73.pdf",
  volume = "II",
}
@techreport{TTPCaseStudy,
  title = "{TTP: A case study in combining induction and data independence}",
  author = "A. W. Roscoe and S.J. Creese",
  year = "1999",
  institution = "{Oxford University Computing Laboratory}",
  number = "{PRG-TR-1-99}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/74.ps",
}
@article{dataIndependenceTechniques,
  title = "Proving security protocols with model checkers by data independence techniques",
  author = "A. W. Roscoe and P.J. Broadfoot",
  year = "1999",
  journal = "{Journal of Computer Security}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/70.pdf",
  volume = "7",
}
@inproceedings{provingSecurityProtocols,
  title = "Proving security protocols with model checkers by data independence techniques",
  author = "A. W. Roscoe",
  year = "1998",
  booktitle = "{Proceedings of CSFW 1998}",
  publisher = "{IEEE Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/67.pdf",
}
@book{theoryAndPractice,
  title = "The theory and practice of concurrency",
  author = "A. W. Roscoe",
  year = "1998",
  isbn = "0-13-6774409-5",
  note = "The text book teaching material can be found at \url{http://www.comlab.ox.ac.uk/publications/books/concurrency/}",
  publisher = "{Prentice Hall}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf",
}
@inproceedings{verifyingDeterminism,
  title = "{Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays}",
  author = "A. W. Roscoe and R. Lazic",
  year = "1998",
  booktitle = "Proceedings of {INFINITY'98}",
  month = "July",
  note = "{extended version as Oxford University Computing Laboratory TR-2-98.}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/66.ps",
}
@inbook{specificationOfAParallelSystem,
  title = "{A Case Study of the Formal Specification of a Parallel System using CSP}",
  author = "A. W. Roscoe and S. Kiyamura",
  year = "1997",
  booktitle = "Correct Models of Parallel Computing",
  editor = "S. Noguchi and M. Ota",
  publisher = "{IOS Press}",
}
@techreport{timed-failures-stability,
  title = "{The timed failures-stability model for Timed CSP}",
  author = "A. W. Roscoe and G.M. Reed",
  year = "1996",
  institution = "{Oxford University Computing Laboratory}",
  note = "also appeared in Theoretical Computer Science, Vol 211 (1999)",
  number = "{PRG-119}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/60.pdf",
}
@article{journals/tcs/Lowe95,
  title = "Probabilistic and Prioritized Models of Timed CSP",
  author = "Gavin Lowe",
  year = "1995",
  journal = "Theor. Comput. Sci.",
  number = "2",
  pages = "315-352",
  url = "http://www.cs.ox.ac.uk/people/gavin.lowe/Papers/Probs/MFPS.ps.gz",
  volume = "138",
  doi = "10.1016/0304-3975(94)00171-E",
}
@article{journals/cj/Lowe95,
  title = "Scheduling-Oriented Models for Real-Time Systems",
  author = "Gavin Lowe",
  year = "1995",
  journal = "The Computer Journal",
  number = "6",
  pages = "443-456",
  url = "http://www.cs.ox.ac.uk/people/gavin.lowe/Papers/TAM/scheduling.ps.gz",
  volume = "38",
}
@article{journals/cj/LoweZ95,
  title = "Refinement of Complex Systems: A Case Study",
  author = "Gavin Lowe and Hussein Zedan",
  year = "1995",
  journal = "The Computer Journal",
  number = "10",
  pages = "785-800",
  url = "http://www.cs.ox.ac.uk/people/gavin.lowe/Papers/TAM/casestudy.ps.gz",
  volume = "38",
}
@inproceedings{HierarchicalCompression,
  title = "{Hierarchical compression for model-checking CSP, or How to check 10^{20} dining philosophers for deadlock}",
  author = "A. W. Roscoe and P.H.B. Gardiner, M.H. Goldsmith, J.R. Hulance, D.M.Jackson and J.B. Scattergood",
  year = "1995",
  booktitle = "{Proceedings of TACAS 1995}",
  note = "also revised in a version of these proceedings published by {LNCS}",
  publisher = "{BRICS}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/59.pdf",
}
@article{occam2-2,
  title = "Denotational semantics for occam2, Part 2",
  author = "A. W. Roscoe and M.H. Goldsmith and B.G.O. Scott",
  year = "1994",
  journal = "{Transputer Communications}",
  pages = "25--67",
  series = "1",
  volume = "2",
}
@article{occam2-1,
  title = "Denotational semantics for occam2, Part 1",
  author = "A. W. Roscoe and M.H. Goldsmith and B.G.O. Scott",
  year = "1994",
  journal = "{Transputer Communications}",
  pages = "65--91",
  series = "2",
  volume = "1",
}
@book{ClassicalMindBook,
  title = "{A Classical Mind: essays in Honour of C.A.R. Hoare}",
  year = "1994",
  editor = "A. W. Roscoe",
  isbn = "0132948443",
  publisher = "{Prentice-Hall}",
}
@inbook{ClassicalMindChapter,
  title = "Model-checking {CSP}",
  author = "{A. W. Roscoe}",
  year = "1994",
  booktitle = "{A Classical Mind: essays in Honour of C.A.R. Hoare}",
  chapter = "21",
  publisher = "{Prentice-Hall}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/50.ps",
}
@phdthesis{/thesis/Lowe93,
  title = "{Probabilities and Priorities in Timed CSP}",
  author = "Gavin Lowe",
  year = "1993",
  school = "Oxford University Computing Laboratory",
  url = "http://www.cs.ox.ac.uk/people/gavin.lowe/Papers/Probs/thesis.ps.gz",
}
@techreport{occamdenotational,
  title = "{Denotational semantics for occam II}",
  author = "A. W. Roscoe and M.H. Goldsmith and B.G.O. Scott",
  year = "1993",
  institution = "{Oxford University Computing Laboratory}",
  number = "PRG-108",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/47.pdf",
}
@inproceedings{protocolsInCSP,
  title = "Developing and verifying protocols in {CSP}",
  author = "A. W. Roscoe",
  year = "1993",
  booktitle = "Proceedings of {Mierlo} workshop on protocols",
  publisher = "{TU Eindhoven}",
}
@article{occamMicroprocessors,
  title = "Occam in the specification and verification of microprocessors",
  author = "A. W. Roscoe",
  year = "1992",
  journal = "Phil Trans R. Soc. Lond A",
  note = "{Also in Mechanised Reasoning and Hardware Design, M.J.C. Gordon and C.A.R. Hoare, eds (Prentice-Hall, 1992), extended version available at \url{http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/45ex.ps} }",
  pages = "137-151",
  url = "http://www.jstor.org/view/09628428/ap000030/00a00150/0",
  volume = "339",
}
@inproceedings{timedCSPtheory,
  title = "{Timed CSP: theory and practice}",
  author = "A. W. Roscoe and J.Davies and D.Jackson and G.M.Reed and J.Reed and S.A. Schneider",
  year = "1992",
  booktitle = "Proceedings of {REX} Workshop",
  publisher = "LNCS",
  volume = "600",
}
@article{AnalysingTMFS,
  title = "{Analysing TM_{FS}: a study of nondeterminism in real-time concurrency}",
  author = "A. W. Roscoe and G.M. Reed",
  year = "1991",
  editor = "Yonezawa and Ito",
  journal = "{Concurrency: Theory Language and Architecture}",
  publisher = "Springer LNCS",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/38.ps",
  volume = "491",
}
@article{occamsemantic,
  title = "{A semantic model for occam II}",
  author = "A. W. Roscoe and M.H. Goldsmith and B.G.O. Scott",
  year = "1991",
  journal = "Proceedings of Transputing",
  volume = "93",
}
@article{DeadlockAnalysis2,
  title = "Deadlock analysis in networks of communicating processes",
  author = "A. W. Roscoe and S.D. Brookes",
  year = "1991",
  journal = "Distributed Computing",
  number = "4",
  pages = "209--230",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/30.pdf",
}
@inproceedings{timewiseRefinement,
  title = "{CSP} and timewise refinement",
  author = "A. W. Roscoe and G. M. Reed and S. A. Schneider",
  year = "1991",
  booktitle = "{Proceedings of the BCS-FACS Refinement Workshop}",
  publisher = "LNCS",
}
@techreport{MaintainingConsistency,
  title = "Maintaining consistency in distributed databases",
  author = "A. W. Roscoe",
  year = "1990",
  institution = "{Oxford University Computing Laboratory}",
  number = "{PRG-87}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/33.ps",
}
@techreport{CommunicationAndCorrectness,
  title = "Communication and correctness in {Timed CSP}",
  author = "A. W. Roscoe and S.A. Schneider and J.W. Davies and D.M. Jackson and G.M. Reed",
  year = "1990",
  institution = "Esprit SPEC project",
}
@techreport{TemporalLogic,
  title = "A temporal logic for {Timed CSP}",
  author = "D.M. Jackson and J.W. Davies and G.M. Reed and S.A. Schneider",
  year = "1990",
  institution = "{Esprit SPEC project}",
}
@inproceedings{UnboundedNondeterminism2,
  title = "Unbounded nondeterminism in {CSP}",
  author = "A. W. Roscoe and G.Barrett",
  year = "1989",
  booktitle = "Proceedings of MFPS89",
  number = "298",
  publisher = "Springer",
  series = "LNCS",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/29.pdf",
}
@article{ATimedModel,
  title = "A timed model for communicating sequential processes",
  author = "A. W. Roscoe and G.M. Reed",
  year = "1988",
  journal = "{Theoretical Computer Science}",
  pages = "249--261",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/23.pdf",
  volume = "58",
}
@article{LawsOfOccamProgramming,
  title = "The laws of occam programming",
  author = "A. W. Roscoe and C.A.R. Hoare",
  year = "1988",
  journal = "Theoretical Computer Science",
  note = "Previously appeared as Oxford University Computing Laboratory Technical Report PRG-53, 1986.",
  pages = "177--229",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/24.pdf",
  volume = "60",
}
@techreport{UnboundedNondeterminism1,
  title = "Unbounded nondeterminism in {CSP}",
  author = "A. W. Roscoe",
  year = "1988",
  institution = "{Oxford University Computing Laboratory}",
  month = "July",
  note = "in \emph{Two papers on CSP}, Also appeared in Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993)",
  number = "PRG-67",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/28.ps",
}
@inproceedings{TransformingOccamPrograms,
  title = "Transforming occam programs",
  author = "A. W. Roscoe and M.H. Goldsmith",
  year = "1988",
  booktitle = "{The Design and Application of Parallel Digital Processors}",
  number = "298",
  series = "{IEE Conference Publication}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/22.pdf",
}
@inproceedings{MetricSpaces,
  title = "Metric spaces as models for real-time concurrency",
  author = "A. W. Roscoe and G.M. Reed",
  year = "1988",
  booktitle = "{Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans, 1987)}",
  editor = "Main et al",
  number = "298",
  pages = "331--343",
  publisher = "Springer",
  series = "LNCS",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/19.pdf",
}
@techreport{AlternativeOrder,
  title = "An alternative order for the failures model",
  author = "A. W. Roscoe",
  year = "1988",
  institution = "{Oxford University Computing Laboratory}",
  month = "July",
  note = "in \emph{Two papers on CSP}, Also appeared in Journal of Logic and Computation 2, 5 pp557-577",
  number = "PRG-67",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/27.ps",
}
@article{PursuitDeadlockFreedom,
  title = "The pursuit of deadlock freedom",
  author = "A. W. Roscoe and Naiem Dathi",
  year = "1987",
  journal = "{Information and Computation}",
  month = "December",
  number = "3",
  pages = "289--327",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/18.ps",
  volume = "75",
}
@inproceedings{RoutingMessages,
  title = "Routing messages through networks: an exercise in deadlock avoidance",
  author = "A. W. Roscoe",
  year = "1987",
  address = "Amsterdam",
  booktitle = "{Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting}",
  editor = "Muntean et al.",
  publisher = "{IOS B.V.}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/21.ps",
}
@techreport{OperationSemanticsCSP,
  title = "An Operational Semantics for {CSP}",
  author = "A. W. Roscoe and S. D. Brookes and D. J. Walker",
  year = "1986",
  institution = "{Oxford University Computing Laboratory}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/26.ps",
}
@inproceedings{TimedModel,
  title = "A timed model for communicating sequential processes",
  author = "A. W. Roscoe and G.M. Reed",
  year = "1986",
  booktitle = "{Proc.ICALP 86}",
  number = "226",
  pages = "314--323",
  publisher = "Springer",
  series = "{LNCS}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/17.pdf",
}
@inproceedings{SpecifyingProblemOne,
  title = "Specifying problem one using the failures model for {CSP} and deriving {CSP} processes which meet this specification",
  author = "A. W. Roscoe",
  year = "1985",
  booktitle = "{The Analysis of Concurrent Systems}",
  editor = "B.T. Denvir et al",
  number = "207",
  pages = "103--109",
  publisher = "Springer",
  series = "{LNCS}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/14.pdf",
}
@proceedings{PittsburghSeminarConcurrency,
  title = "Proceedings of the {Pittsburgh} seminar on concurrency",
  year = "1985",
  editor = "A. W. Roscoe and S.D. Brookes and G. Winskel",
  number = "197",
  publisher = "Springer",
  series = "LNCS",
  url = "http://www.springerlink.com/content/l11x0377l276/?p=888bb7ca2d8845db84c4663e9e7407e0&pi=0",
}
@inproceedings{DenotationalSemanticsOccam,
  title = "Denotational semantics for occam",
  author = "A. W. Roscoe",
  year = "1985",
  booktitle = "Proceedings of the {Pittsburgh} seminar on concurrency",
  number = "197",
  pages = "306--329",
  publisher = "Springer",
  series = "LNCS",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/10.pdf",
}
@inproceedings{DeadlockAnalysis,
  title = "Deadlock analysis in networks of communicating processes",
  author = "A. W. Roscoe and S.D. Brookes",
  year = "1985",
  booktitle = "{Logics and Models of Concurrent Systems}",
  editor = "K.R. Apt",
  pages = "305--324",
  publisher = "Springer",
  series = "NATO ASI series F",
  volume = "13",
}
@inproceedings{AnImprovedFailuresModel,
  title = "An improved failures model for communicating processes",
  author = "A. W. Roscoe and S.D. Brookes",
  year = "1985",
  booktitle = "Proceedings of the {Pittsburgh} seminar on concurrency",
  number = "197",
  pages = "281--305",
  publisher = "Springer",
  series = "LNCS",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/9.pdf",
}
@inproceedings{Trains,
  title = "A {CSP} solution to the \emph{trains} problem",
  author = "A. W. Roscoe",
  year = "1985",
  booktitle = "{The Analysis of Concurrent Systems}",
  editor = "B.T. Denvir et al",
  number = "207",
  pages = "384--388",
  publisher = "Springer",
  series = "{LNCS}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/15.pdf",
}
@article{ATheoryofCSP,
  title = "A theory of communicating sequential processes",
  author = "A. W. Roscoe and S.D. Brookes and C.A.R. Hoare",
  year = "1984",
  journal = "{Journal of the ACM}",
  month = "July",
  number = "3",
  pages = "560--599",
  series = "31",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/4.pdf",
}
@inproceedings{ExecutablePredicates,
  title = "Programs as executable predicates",
  author = "A. W. Roscoe and C.A.R. Hoare",
  year = "1984",
  booktitle = "{Proceedings of FGCS84 (ICOT, editors)}",
  pages = "220--228",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/5.pdf",
}
@phdthesis{AMathematicalTheory,
  title = "A mathematical theory of communicating processes",
  author = "A. W. Roscoe",
  year = "1982",
  note = "Please note this is a 270 page, 118 Mb scanned file and will take some time to download.",
  school = "Oxford University",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/2.pdf",
}
@techreport{ATheory,
  title = "A theory of communicating sequential processes",
  author = "A. W. Roscoe and S.D. Brookes and C. A. R. Hoare",
  year = "1981",
  institution = "Oxford University Computing Laboratory",
  month = "May",
  number = "{PRG-16}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/1.pdf",
}