@article{socialhisp12,
  title = "Social networks for importing and exporting security",
  author = "Bangdao Chen and A.W. Roscoe",
  year = "2012",
  booktitle = "Proceedings of 2012 Monterey Workshop",
  publisher = "Springer",
  series = "LNCS (to appear)",
}
@article{Roscoe2012priority,
  title = "Fairness analysis through priority",
  author = "P. Armstrong, P.J. Hopcroft and A.W. Roscoe",
  year = "2012",
}
@article{Roscoe2012FSE,
  title = "Short-output universal hash functions and their use in fast and secure message authentication",
  author = "Nguyen, L.H. and Roscoe, A.W.",
  year = "2012",
  journal = "FSE 2012 � to appear",
  url = "http://eprint.iacr.org/2011/116.pdf",
}
@article{Roscoe2012FDR},
  title = "Recent developments in FDR",
  author = "Armstrong, P. and Goldsmith, M.H. and Lowe, G. and Ouaknine, J. and Palikareva, H. and Roscoe, A. and Worrell, J.",
  year = "2012",
  journal = "CAV 2012 � to appear",
}
@article{roscoe2012timedni,
  title = "Checking noninterference in the timed world",
  author = "Roscoe, A.W and Huang, J.",
  year = "2012",
}
@article{roscoe2012timed,
  title = "Model checking Timed CSP",
  author = "Armstrong, P. and  Lowe, G. and Ouaknine, J and Roscoe, A.W",
  year = "2012",
  booktitle = "In Proceedings of HOWARD (Festschrift for Howard Barringer)",
}
@article{springerlink:10.1007/s11036-012-0366-2,
  title = "Reverse Authentication in Financial Transactions and Identity Management",
  author = "Chen, Bangdao and Nguyen, Long and Roscoe, A.W.",
  year = "2012",
  affiliation = "Department of Computer Science, Oxford University, Oxford, UK",
  issn = "1383-469X",
  journal = "Mobile Networks and Applications",
  note = "10.1007/s11036-012-0366-2",
  pages = "1-16",
  publisher = "Springer Netherlands",
  url = "http://dx.doi.org/10.1007/s11036-012-0366-2",
}
@article{roscoe2011model,
  title = "Model checking cryptographic protocols subject to combinatorial attack",
  author = "Roscoe, A.W. and Smyth, T. and Nguyen, L.",
  year = "2012",
}
@article{ouaknine2011static,
  title = "Static livelock analysis in CSP",
  author = "Ouaknine, J. and Palikareva, H. and Roscoe, A. and Worrell, J.",
  year = "2011",
  journal = "CONCUR 2011--Concurrency Theory",
  pages = "389--403",
  publisher = "Springer",
  url = "http://www.springerlink.com/content/a14672716755020g/",
}
@article{chen2011context,
  title = "When Context Is Better Than Identity: Authentication by Context Using Empirical Channels",
  author = "Chen, B. and Nguyen, L. and Roscoe, A.",
  year = "2011",
  journal = "Security Protocols XIX",
  pages = "115--125",
  publisher = "Springer",
}
@article{palikareva2011sat,
  title = "SAT-solving in CSP trace refinement",
  author = "Palikareva, H. and Ouaknine, J. and Roscoe, A.W.",
  year = "2011",
  journal = "Science of Computer Programming",
  publisher = "Elsevier",
  url = "http://www.sciencedirect.com/science/article/pii/S0167642311001547",
}
@inproceedings{huang2011body,
  title = "Body sensor network key distribution using human interactive channels",
  author = "Huang, X. and Wang, Q. and Chen, B. and Markham, A. and J{\"a}ntti, R. and Roscoe, A.W.",
  year = "2011",
  booktitle = "Proceedings of the 4th International Symposium on Applied Sciences in Biomedical and Communication Technologies",
  organization = "ACM",
  pages = "143",
  doi = "http://dx.doi.org/10.1145/2093698.2093841",
}
@inproceedings{khattri2011translating,
  title = "Translating Timed Automata to Tock-CSP",
  author = "Khattri, M. and Roscoe, A.W. and Ouaknine, J.",
  year = "2011",
  booktitle = "Parallel and Distributed Computing and Networks/720: Software Engineering",
  organization = "ACTA Press",
}
@inproceedings{wistp11,
  title = "Mobile Electronic Identity: Securing Payment on Mobile Phones",
  author = "Chen Bangdao and A.W. Roscoe",
  year = "2011",
  note = "Proceedings of WISTP 2011",
}
@article{Ros126,
  title = "Authentication protocols based on low-bandwidth unspoofable channels: a comparative survey",
  author = "L.H. Nguyen and A.W. Roscoe",
  year = "2011",
  journal = "Journal of Computer Security",
  volume = "19",
}
@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).",
}
@inproceedings{kainda2010secure,
  title = "Secure mobile ad-hoc interactions: reasoning about out-of-band (oob) channels",
  author = "Kainda, R. and Flechais, I. and Roscoe, AW",
  year = "2010",
  booktitle = "In Second International Workshop on Security and Privacy in Spontaneous Interaction and Mobile Phone Use (IWSSI/SPMU)",
  url = "http://www.springerlink.com/content/kt1222483260p714/",
}
@inproceedings{kainda2010two,
  title = "Two heads are better than one: security and usability of device associations in group scenarios",
  author = "Kainda, R. and Flechais, I. and Roscoe, A.W.",
  year = "2010",
  booktitle = "Proceedings of the Sixth Symposium on Usable Privacy and Security",
  organization = "ACM",
  pages = "5",
}
@inproceedings{misslk,
  title = "The missing link: Human Interactive Security Protocols in mobile payment",
  author = "Chen Bangdao, L.H. Nguyen and  A.W. Roscoe",
  year = "2010",
  note = "In Proceedings of  5th International Workshop on Security, Kobe, Japan",
}
@inproceedings{RevAuthFT,
  title = "Reverse authentication in financial transactions",
  author = "Chen Bangdao and A.W. Roscoe",
  year = "2010",
  note = "In Proceedings of IWSSI/SPMU, Helsinki",
}
@techreport{3969,
  title = "A new bound for t-wise almost universal hash functions",
  author = "L.H. Nguyen and A.W. Roscoe",
  year = "2010",
  institution = "OUCL",
  month = "November",
  number = "RR-10-24",
  pages = "4",
}
@book{awr135,
  title = "Understanding Concurrent Systems",
  author = "A.W. Roscoe",
  year = "2010",
  isbn = "978-1-84882-257-3",
  publisher = "Springer",
  size = "533pp",
  url = "http://www.comlab.ox.ac.uk/ucs",
}
@article{Ros135,
  title = "Security and Usability: Analysis and Evaluation",
  author = "Ronald Kainda and Ivan Flechais and A.W. Roscoe",
  year = "2010",
  booktitle = "Proceedings of ARES 2010",
}
@article{Ros133,
  title = "Secure and usable out-of-band channels for ad hoc mobile device interactions",
  author = "Kainda, R. and Flechais, I. and Roscoe, A.W.",
  year = "2010",
  booktitle = "Proceedings of WISTP 2010",
  publisher = "Springer",
}
@book{Ros132,
  title = "Reflections on the work of C.A.R. Hoare",
  author = "C.B. Jones, A.W. Roscoe and K.R. Wood (editors)",
  year = "2010",
  publisher = "Springer",
  series = "History of computing",
}
@article{Ros131,
  title = "Insight, innovation and collaboration",
  author = "C.B. Jones and A.W. Roscoe",
  year = "2010",
  booktitle = "Reflections on the work of C.A.R. Hoare",
  publisher = "Springer",
}
@article{Ros127,
  title = "CSP is expressive enough for pi",
  author = "A.W. Roscoe",
  year = "2010",
  booktitle = "to appear in Reflections on the work of C.A.R. Hoare",
  editor = "C.B. Jones, A.W. Roscoe and K.R. Wood",
  publisher = "Springer",
}
@article{Ros130,
  title = "Local search in model checking",
  author = "A.W. Roscoe, P.J. Armstrong and Pragyesh",
  year = "2009",
  booktitle = "To appear in Proc ATVA 2009 (Springer)",
}
@article{Ros128,
  title = "New combinatorial bounds for universal hash functions",
  author = "L.H. Nguyen and A.W. Roscoe",
  year = "2009",
}
@article{Ros129,
  title = "Usability and security of out-of-bound channels in secure device pairing protocols",
  author = "R. Kainda, I. Flechais and A.W. Roscoe",
  year = "2009",
  booktitle = "Proceedings of SOUPS 2009",
}
@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{biro122,
  title = "Separating two roles of hashing in one-way message authentication",
  author = "L.H. Nguyen and A.W. Roscoe",
  year = "2008",
  booktitle = "Proceedings of FCS-ARSPA-WITS",
  note = "(This version is extended by appendices not present in proceedings.)",
}
@inproceedings{biro121,
  title = "The three Platonic models of divergence-strict CSP",
  author = "A.W. Roscoe",
  year = "2008",
  booktitle = "Proceedings of ICTAC '08",
}
@article{ShortDigests,
  title = "Authenticating ad hoc networks by comparison of short digests",
  author = "A. W. Roscoe and L. H. Nguyen",
  year = "2008",
  journal = "{Information and Computation}",
  pages = "250-271",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/120.pdf",
  volume = "206",
}
@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{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{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",
}
@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",
}
@inproceedings{EfficientGroupAuthentication,
  title = "Efficient group authentication protocols based on human interaction",
  author = "A. W. Roscoe and L. H. Nguyen",
  year = "2006",
  booktitle = "{Proceedings of ARSPA 2006}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/116.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}",
  note = "scripts: \url{http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/115.csp}; \url{http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/115statechartcompiler.csp}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/115.pdf",
}
@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",
}
@unpublished{Human-centred,
  title = "Human-centred computer security",
  author = "A. W. Roscoe",
  year = "2006",
  note = "Unpublished draft",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/113.pdf",
}
@inproceedings{Multi-Party,
  title = "Bootstrapping Multi-Party Ad-Hoc Security",
  author = "A. W. Roscoe and S. J. Creese and M. H. Goldsmith and Ming Xiao",
  year = "2006",
  booktitle = "{Proceedings of SAC 2006}",
  note = "to appear",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/111.pdf",
}
@inproceedings{TimedWorld,
  title = "Extending noninterference properties to the timed world",
  author = "A. W. Roscoe and Jian Huang",
  year = "2006",
  booktitle = "{Proceedings of SAC 2006}",
  note = "to appear",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/110.pdf",
}
@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{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{UbiquiousCommunication,
  title = "Security and trust for ubiquitous communication",
  author = "A. W. Roscoe and Sadie Creese and Mike Reed and Jeff Sanders",
  year = "2005",
  booktitle = "{ITU WSIS Thematic Meeting on Cybersecurity, Geneva, Switzerland}",
  month = "June",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/108.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",
}
@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",
}
@inproceedings{RelationshipProtocols,
  title = "On the relationship between {Web Services Security} and traditional protocols",
  author = "A. W. Roscoe and Eldar Kleiner",
  year = "2005",
  booktitle = "{Proceedings of MFPS 2005}",
  note = "To appear.",
  url = "href="http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/104.pdf",
}
@inproceedings{Exploiting,
  title = "Exploiting Empirical Engagement in Authentication Protocol Design",
  author = "Sadie Creese and Michael Goldsmith and Richard Harrison and Bill Roscoe and Paul Whittaker and Irfan Zakiuddin",
  year = "2005",
  booktitle = "Proceedings of SPPC 2005",
  month = "May",
}
@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",
}
@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{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{WebServicesSecurity,
  title = "{Web Services Security: a preliminary study using Casper and FDR}",
  author = "A. W. Roscoe and E. Kleiner",
  year = "2004",
  booktitle = "{Proceedings of Automated Reasoning for Security Protocol Analysis (ARSPA 04)}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/100.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",
}
@inproceedings{human-centric-directions,
  title = "Research directions for trust and security in human-centric computing",
  author = "A. W. Roscoe and Sadie Creese and Michael Goldsmith and Irfan Zakiuddin",
  year = "2004",
  booktitle = "{Proceedings of SPPC 2004}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/97.pdf",
}
@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",
}
@article{EmbeddingAgents,
  title = "Embedding agents within the intruder to detect parallel attacks",
  author = "A. W. Roscoe and P.J. Broadfoot",
  year = "2004",
  journal = "{Journal of Computer Security}",
  number = "3-4",
  pages = "379-408",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/86.pdf",
  volume = "12",
}
@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",
}
@inproceedings{PervasiveComputing,
  title = "Authentication in pervasive computing",
  author = "A. W. Roscoe and S.J. Creese and M.H. Goldsmith and I.Zakiuddin",
  year = "2003",
  booktitle = "Proceedings of the First International Conference on Security in Pervasive Computing",
  month = "March",
  publisher = "{LNCS}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/87.ps",
}
@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",
}
@inproceedings{TheAttacker,
  title = "The attacker in ubiquitous computing environments: formalising the threat model",
  author = "A. W. Roscoe and S.J. Creese and M.H. Goldsmith and I.Zakiuddin",
  year = "2003",
  booktitle = "{Proceedings of FAST 2003, Pisa}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/92.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",
}
@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",
}
@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",
}
@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{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{Compiling,
  title = "{Compiling Shared Variable Programs into CSP}",
  author = "A. W. Roscoe",
  year = "2001",
  booktitle = "{Proceedings of PROGRESS workshop 2001}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/82.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{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",
}
@book{SecurityProtocolsBook,
  title = "The Modelling and Analysis of Security Protocols",
  author = "A. W. Roscoe and P. Ryan and S. Schneider and M. Goldsmith and G. Lowe",
  year = "2001",
  publisher = "{Addison-Wesley}",
}
@book{MillenialPerspectives,
  title = "{Millennial Perspectives in Computer Science}",
  year = "2000",
  editor = "A. W. Roscoe and J. Davies and J. Woodcock",
  publisher = "{Palgrave}",
}
@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{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",
}
@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)}",
  month = "June",
  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",
}
@inproceedings{InfiniteFamilyOfInductions,
  title = "{Verifying an infinite family of inductions simultaneously using data independence and FDR}",
  author = "A. W. Roscoe and S.J. Creese",
  year = "1999",
  booktitle = "{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)}",
  publisher = "{Kluwer Academic Publishers}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/72.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",
}
@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{intransitiveNoninterference,
  title = "What is intransitive noninterference?",
  author = "A. W. Roscoe and M.H. Goldsmith",
  year = "1999",
  booktitle = "{Proceedings of CSFW 1999}",
  publisher = "{IEEE Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/69.ps",
}
@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{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",
}
@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}",
}
@inproceedings{perfectspy,
  title = "The perfect spy for model-checking crypto-protocols",
  author = "A. W. Roscoe and M.H. Goldsmith",
  year = "1997",
  booktitle = "{Proceedings of DIMACS workshop on the design and formal verification of crypto-protocols}",
  note = "\url{http://dimacs.rutgers.edu/workshops/program2/program.html}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/63.pdf",
}
@techreport{TMNProtocol,
  title = "{Using CSP to detect errors in the TMN protocol}",
  author = "A. W. Roscoe and G. Lowe",
  year = "1996",
  institution = "{University of Leicester}",
  note = "{and IEEE transactions on Software Engineering Vol 23 (1997)}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/65.ps",
}
@article{non-well-founded-sets,
  title = "On transition systems and non-well-founded sets",
  author = "A. W. Roscoe and R.S. Lazic",
  year = "1996",
  journal = "Annals of the New York Academiy of Sciences",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/62.pdf",
  volume = "806",
}
@inproceedings{IntensionalSpecifications,
  title = "Intensional specifications of security protocols",
  author = "A. W. Roscoe",
  year = "1996",
  booktitle = "{Proceedings of 1996 IEEE Computer Security Foundations Workshop}",
  publisher = "{IEEE Computer Society Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/61.ps",
}
@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",
}
@inproceedings{CSPandDeterminism,
  title = "{CSP} and determinism in security modelling",
  author = "1996",
  year = "1996",
  booktitle = "{Proceedings of 1995 IEEE Symposium on Security and Privacy}",
  publisher = "{IEEE Computer Society Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/56.ps",
}
@article{NoninterferenceRevised,
  title = "Non-interference through determinism",
  author = "A. W. Roscoe and J.C.P. Woodcock and L. Wulf",
  year = "1996",
  journal = "{Journal of Computer Security}",
  note = "revised version of above",
  pages = "27--54",
  series = "1",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/55.pdf",
  volume = "4",
}
@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",
}
@inproceedings{key-exchange,
  title = "{Modelling and verifying key-exchange protocols using CSP and FDR}",
  author = "A. W. Roscoe",
  year = "1995",
  booktitle = "{Proceedings of 1995 IEEE Computer Security Foundations Workshop}",
  publisher = "{IEEE Computer Society Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/58.ps",
}
@inproceedings{ComposingAndDecomposing,
  title = "Composing and decomposing systems under security properties",
  author = "A. W. Roscoe and L. Wulf",
  year = "1995",
  booktitle = "{Proceedings of 1995 IEEE Computer Security Foundations Workshop}",
  publisher = "{IEEE Computer Society Press}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/57.ps",
}
@inproceedings{Noninterference,
  title = "Non-interference through determinism",
  author = "A. W. Roscoe and J.C.P. Woodcock and L. Wulf",
  year = "1994",
  booktitle = "{Proceedings of ESORICS 94}",
  series = "{LNCS 875}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/54.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",
  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",
}
@article{FixedPoints,
  title = "Fixed points without completeness",
  author = "A. W. Roscoe and M.W. Mislove and S.A. Schneider",
  year = "1993",
  chapter = "2",
  journal = "{Theoretical Computer Science}",
  pages = "273--314",
  volume = "138",
}
@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}",
}
@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",
}
@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",
}
@article{acyclic,
  title = "Acyclic monotone normality",
  author = "A. W. Roscoe and P. Moody",
  year = "1992",
  journal = "Topology and its Applications",
  pages = "53-67",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/44.pdf",
  volume = "47",
}
@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{digitalTopology,
  title = "Concepts of digital topology",
  author = "A. W. Roscoe and T.Y. Kong",
  year = "1992",
  journal = "Topology and its applications",
  pages = "219--262",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/42.pdf",
  volume = "46",
}
@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",
}
@inproceedings{h1transputer,
  title = "Formal methods in the development of the {H1 Transputer}",
  author = "A. W. Roscoe and A.D.B. Cox and M.H. Goldsmith and J.B. Scattergood",
  year = "1991",
  booktitle = "{Proceedings of Transputing 91}",
  publisher = "IOS",
}
@article{starCovering,
  title = "Star covering properties",
  author = "A. W. Roscoe and E.K. van Douwen and G.M. Reed and I.J. Tree",
  year = "1991",
  journal = "Topology and its Applications",
  pages = "71-103",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/40.pdf",
  volume = "39",
}
@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",
}
@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",
}
@proceedings{topologyAndCategory,
  title = "Topology and category theory in computer science",
  year = "1991",
  editor = "A. W. Roscoe and G.M. Reed and R.F. Wachter",
  note = "proceedings of a special session at the 1989 Oxford Topology Conference",
  publisher = "{OUP}",
}
@inbook{topology,
  title = "Topology, computer science and the mathematics of convergence",
  author = "A. W. Roscoe",
  year = "1991",
  booktitle = "Topology and Category Theory in Computer Science",
  editor = "G.M. Reed and A. W. Roscoe and R.F. Wachter",
  publisher = "{OUP}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/36.ps",
}
@article{LatticeConditionsII,
  title = "A lattice of conditions on topological spaces {II}",
  author = "A. W. Roscoe and P. Moody and G.M. Reed and P.J. Collins",
  year = "1991",
  journal = "Fundamenta Mathematicae",
  number = "138",
  pages = "69--81",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/31.pdf",
}
@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",
}
@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}",
}
@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{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",
}
@inbook{PointCountableBaseProblem,
  title = "The point-countable base problem",
  author = "A. W. Rosoce and P.J. Collins and G.M. Reed",
  year = "1990",
  booktitle = "Problems in Topology",
  editor = "G.M. Reed and J. van Mill",
  publisher = "Elsevier",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/32.pdf",
}
@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",
}
@unpublished{DomainTheoryNotes,
  title = "Notes on Domain Theory",
  author = "A. W. Roscoe",
  year = "1989",
  note = "These notes were written for the Oxford Domain Theory course between 1984 and 1989.  I originally planned to publish them as half of "Domains for denotational semantics".",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/domnotes.pdf",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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",
}
@article{LawsOfProgramming,
  title = "Laws of programming",
  author = "A. W. Roscoe and C.A.R. Hoare and He Jifeng and I.J. Hayes and C.C. Morgan and J.W. Sanders and I.H. Sorensen and J.M. Spivey and B.A. Sufrin",
  year = "1987",
  journal = "{Communications of the ACM}",
  month = "August",
  note = "Previously appeared as Oxford University Computing Laboratory Technical Report PRG-42.",
  number = "8",
  pages = "672--686",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/20.pdf",
  volume = "30",
}
@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",
}
@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",
}
@techreport{DecompositionOfRectangle,
  title = "The decomposition of a rectangle into rectangles of minimal perimeter",
  author = "A. W. Roscoe and T.Y. Kong and D.M. Mount",
  year = "1986",
  institution = "{University of Maryland Center for Automation Research}",
  note = "Also SIAM Journal of Computing 17, 6 pp1215-1231.",
  number = "{CAR-TR-169}",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/25.pdf",
}
@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",
}
@article{LocalSymmetry,
  title = "Local symmetry and triangle laws are sufficient for metrisability",
  author = "A. W. Roscoe and P.J. Collins",
  year = "1985",
  journal = "{Colloquia Mathematica Societatis Janos Bolyai 41}",
  pages = "177--181",
  url = "http://ww.cs.ox.ac.uk/people/bill.roscoe/publications/16.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",
}
@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",
}
@article{BinaryDigitalPictures,
  title = "A theory of binary digital pictures",
  author = "A. W. Roscoe and T.Y. Kong",
  year = "1985",
  journal = "Computer Vision, Graphics and Image Processing",
  month = "November",
  number = "32",
  pages = "221--243",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/13.pdf",
}
@article{SimplyConnectedPolyhedra,
  title = "Characterisations of simply-connected finite polyhedra in 3-space",
  author = "A. W. Roscoe and T.Y. Kong",
  year = "1985",
  journal = "{Bull. London Math. Soc.}",
  month = "November",
  number = "17",
  pages = "575--578",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/12.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{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{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",
}
@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",
}
@article{LatticeOfConditions,
  title = "A lattice of conditions on topological spaces",
  author = "A. W. Roscoe and P.J. Collins and G.M. Reed and M.E. Rudin",
  year = "1985",
  journal = "{Proc. Amer. Math. Soc.}",
  month = "July",
  number = "94",
  pages = "487--496",
  url = "http://www.jstor.org/view/00029939/di970933/97p0219l/0",
}
@article{ContinuousAnalogues,
  title = "Continuous analogues of axiomatised digital surfaces",
  author = "A. W. Roscoe and T.Y. Kong",
  year = "1985",
  journal = "{Computer Vision, Graphics and Image Processing}",
  month = "January",
  number = "29",
  pages = "60--86",
  url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/6.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",
}
@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",
}
@article{MetrisabilityCriteria,
  title = "Criteria for metrisability",
  author = "A. W. Roscoe and P.J. Collins",
  year = "1984",
  journal = "{Proc. Amer. Math. Soc.}",
  month = "April",
  number = "90",
  pages = "631-640",
  url = "http://www.jstor.org/view/00029939/di970918/97p0476c/0",
}
@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",
}