Bill Roscoe : Publications
Click here to download all publications in a single bibtex file
@article{CSPPract,
title = "CSP: a practical process algebra",
author = "S.D. Brookes and A.W. Roscoe",
year = "2021",
}
@article{partfairex,
title = "Partially fair computation from timed release encryption and oblivious transfer",
author = "Geoffroy Couteau and PYA Ryan and A.W. Roscoe",
year = "2021",
howpublished = "To appear in proceedings of ACISP-21",
url = "https://eprint.iacr.org/2019/1281",
}
@article{pedroscver,
title = "Solidifer: bounded model checking Solidity using lazy contract deployment and precise memory modelling",
author = "Pedro Antonino and A.W. Roscoe",
year = "2021",
journal = "Symposium on Applied Computing (SAC) 2021",
}
@article{Lindacnn,
title = "Neural Network Security: Hiding CNN Parameters with Guided Grad-CAM",
author = "Linda Guiga and A.W. Roscoe",
year = "2020",
booktitle = "Proceedings of ICISSP",
}
@article{formscsol,
title = "Formalising and verifying smart contracts with Solidifier: a bounded model checker for Solidity",
author = "P Antonino and A.W. Roscoe",
year = "2020",
url = "https://arxiv.org/abs/2002.02710",
}
@article{tranmodconc,
title = "Translating between models of concurrency",
author = "D. Mestel and A.W. Roscoe",
year = "2020",
journal = "Acta Informatica",
}
@article{Effvcs,
title = "Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving",
author = "P Antonino, T. Gibson-Robinson and A.W. Roscoe",
year = "2019",
journal = "ACM Transactions on Software Engineering Methods",
url = "https://ora.ox.ac.uk/objects/uuid:25ccd99f-7cf5-45a8-9f00-deab1523eb01",
volume = "18",
}
@article{efvlaba,
title = "Efficient verification of concurrent systems using local analysis based approximations and SAT solving",
author = "P Antonino, T. Gibson-Robinson and A.W. Roscoe",
year = "2019",
booktitle = "Formal Aspects of Computing",
url = "https://link.springer.com/article/10.1007/s00165-019-00483-2",
volume = "31",
}
@article{keyagsp,
title = "Key agreement via protocols",
author = "A.W. Roscoe and Wang Lei",
year = "2019",
booktitle = "Foundations of Security, Protocols and Equational Reasoning",
publisher = "Springer",
series = "LNCS",
url = "https://ora.ox.ac.uk/objects/uuid:9229fcce-1f4d-4d0e-8ea7-d84d44790c28/download_file?file_format=pdf&safe_filename=cathy.pdf&type_of_work=Conference+item",
}
@article{Entmin,
title = "A proof of entropy minimisation for outputs in deletion channels via hidden word statistics",
author = "Arash Atashpendar, David Mestel, A.W. Roscoe, Peter YA Ryan",
year = "2018",
url = "https://arxiv.org/pdf/1807.11609.pdf",
}
@article{Reguard,
title = "Reguard: finding reentrancy bugs in smart contracts",
author = "C. Liu, H. Liu, Z. Cao., Z. Chen, B. Chen and A.W. Roscoe",
year = "2018",
booktitle = "ACM ICSE companion proceedings",
url = "https://dl.acm.org/doi/pdf/10.1145/3183440.3183495?casa_token=0pdvUqUiB-MAAAAA:zPhWFNiA1soNNbULCZWgWGnwuaO6koqU2aXv9r4aNPbSjqIRrlC7upCNTX2AQcRBQdoKR3YJHtEcRQ",
}
@article{Clusteringsuper,
title = "From clustering super sequences to entropy minimising subsequences for single and double deletions",
author = "Arash Atashpendar, Marc Beunardeau, Aisling Conolly, Remi Geraud, David Mestel, A.W. Roscoe, Peter YA Ryan",
year = "2018",
url = "https://arxiv.org/abs/1802.00703",
}
@article{HBMCPAMC,
title = "Process algebra and model checking",
author = "Rance Cleaveland, A.W. Roscoe and Scott Smolka",
year = "2018",
booktitle = "Handbook of Model Checking",
url = "https://www.springer.com/gp/book/9783319105741",
}
@proceedings{FM2018proc,
title = "Proceedings of FM 2018",
author = "K Havelund, J Peleska, A.W. Roscoe and E. de Vink",
year = "2018",
url = "https://www.springer.com/gp/book/9783319955810",
}
@article{nondead,
title = "Checking static properties using conservative approximations to reachability",
author = "Pedro Antonino and Thomas Gibson-Robinson and A.W. Roscoe",
year = "2017",
booktitle = "Proceedings of SBMF 2017",
}
@article{tempsig,
title = "Temporal signature (Draft)",
author = "A.W. Roscoe",
year = "2017",
}
@article{tokentacas,
title = "The automatic detection of token structures and invariants using SAT checking",
author = "Pedro Antonino and Thomas Gibson-Robinson and A.W. Roscoe",
year = "2017",
booktitle = "Proceedings of TACAS 2017",
url = "https://www.conference-publishing.com/program/ETAPS17/APP/talk-etaps17tacas-tacasid123-p.html",
}
@article{auditpake,
title = "Auditable PAKEs: approaching fair exchange without a TTP",
author = "A.W. Roscoe and P.Y.A. Ryan",
year = "2017",
booktitle = "to appear in Proceedings of SPW 2017",
}
@article{patience16,
title = "Card games as pointer structures: case studies in mobile CSP modelling",
author = "A.W. Roscoe",
year = "2016",
}
@article{morestatic,
title = "Tighter reachability criteria for deadlock freedom analysis",
author = "Pedro Antonino and Thomas Gibson-Robinson and A.W. Roscoe",
year = "2016",
booktitle = "Proceedings of FM 2016",
}
@article{buchi,
title = "The relationship between CSP, FDR and Buchi Automata",
author = "A.W. Roscoe and Thomas Gibson-Robinson",
year = "2016",
}
@article{mshift,
title = "Reducing complex CSP models to traces via priority",
author = "David Mestel and A.W. Roscoe",
year = "2016",
journal = "Proceedings of MFPS 2016",
}
@article{brazil,
title = "Rigorous development of component-based systems using component metadata and patterns",
author = "M.V.M. Oliviera, P. Antonino, R. Ramos, A.Sampaio, A. Mota and A.W. Roscoe",
year = "2016",
journal = "Formal Aspects of Computing",
url = "http://link.springer.com/article/10.1007/s00165-016-0375-1",
}
@article{Wbisim,
title = "Computing maximal weak and other bisimulations",
author = "Alexandre Boulgakov and Thomas Gibson-Robinson and A.W. Roscoe",
year = "2016",
booktitle = "Formal Aspects of Computing",
}
@article{DelayHISP,
title = "Detecting failed attacks on human-interactive security protocols",
author = "A.W. Roscoe",
year = "2016",
}
@inproceedings{pedrodeadlock,
title = "Efficient deadlock-freedom checking using local analysis and SAT solving",
author = "Pedro Antonino and Thomas Gibson-Robinson and A.W. Roscoe",
year = "2016",
booktitle = "Proceedings of IFM",
}
@article{FDR3Journal,
title = "FDR3: a parallel refinement checker for CSP",
author = "Thomas Gibson-Robinson and Philip Armstrong and Alexandre Boulgakov and A.W. Roscoe",
year = "2015",
journal = "International Journal on Software Tools for Technology Transfer",
url = "http://dx.doi.org/10.1007/s10009-015-0377-y",
doi = "10.1007/s10009-015-0377-y",
}
@inproceedings{ppocsp,
title = "Practical partial order reduction for CSP",
author = "T. Gibson-Robinson, H. Hansen, A.W. Roscoe and X Wang",
year = "2015",
booktitle = "NASA Formal Methods, 2015",
}
@inproceedings{prisht,
title = "The expressiveness of CSP with priority",
author = "A.W. Roscoe",
year = "2015",
booktitle = "Proceedings of MFPS 2015",
}
@article{pricsp,
title = "On the expressive power of CSP extended by priority",
author = "A.W. Roscoe",
year = "2014",
}
@article{icfem14,
title = "Computing maximal bisimulations",
author = "Alexandre Bougakov and Thomas Gibson Robinson and A.W. Roscoe",
year = "2014",
journal = "Proceedings of ICFEM",
}
@article{CPADeSkill,
title = "Reflections on the need to de-skill CSP",
author = "A.W. Roscoe",
year = "2014",
journal = "Proceedings of CPA 2014",
}
@inproceedings{ComputingMaximalBisimulations,
title = "Computing Maximal Bisimulations",
author = "Alexandre Boulgakov and Thomas Gibson-Robinson and A.W. Roscoe",
year = "2014",
booktitle = "Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Proceedings",
url = "http://dx.doi.org/10.1007/978-3-319-11737-9_2",
doi = "10.1007/978-3-319-11737-9_2",
}
@inproceedings{clusterfdr,
title = "FDR into The Cloud",
author = "Thomas Gibson-Robinson and A.W. Roscoe",
year = "2014",
booktitle = "Communicating Process Architectures",
}
@inproceedings{fdr3,
title = "FDR3 — A Modern Refinement Checker for CSP",
author = "Thomas Gibson-Robinson and Philip Armstrong and Alexandre Boulgakov and A.W. Roscoe",
year = "2014",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
pages = "187-201",
doi = "10.1007/978-3-642-54862-8_13",
}
@article{rosco2013twr,
title = "The automated verification of timewise refinement",
author = "A.W. Roscoe",
year = "2013",
journal = "EIT-CPSE",
}
@article{roscoe2013ph1,
title = "Slow abstraction through priority",
author = "A.W. Roscoe and P.J. Hopcroft",
year = "2013",
journal = "Festschrift for He Jifeng, to appear in LNCS",
}
@article{rosco2013hp,
title = "A Static Analysis Framework for Livelock Freedom in CSP",
author = "Jo{\"e}l Ouaknine and Hristina Palikareva and A. W. Roscoe and James Worrell",
year = "2013",
journal = "Logical Methods in Computer Science",
number = "3",
url = "http://arxiv.org/pdf/1304.7394.pdf",
volume = "9",
doi = "10.2168/LMCS-9(3:24)2013",
}
@article{roscoe2013xh1,
title = "Human interactive secure key and ID exchange protocols in body sensor networks",
author = "Xin Huang Bangdao Chen, Andrew Markham, Quinghua Wang, Zheng Yan, A.W. Roscoe",
year = "2013",
journal = "IET Information Security",
url = "http://ieeexplore.ieee.org/xpl/abstractAuthors.jsp?arnumber=6475237&tag=1",
volume = "7",
}
@article{roscoe2012timedni,
title = "Checking noninterference in the timed world",
author = "Roscoe, A.W and Huang, J.",
year = "2013",
journal = "Formal Aspects of Computing",
volume = "25",
}
@article{roscoe2012ln2,
title = "Reverse authentication in financial transactions and identity management",
author = "Bangdao Chen, L.H. Nguyen and A.W. Roscoe",
year = "2012",
journal = "Mobile Networks and Applications",
url = "http://link.springer.com/article/10.1007/s11036-012-0366-2#page-1",
}
@article{roscoe2012ln1,
title = "Simple construction of epsilon-biased distribution",
author = "L.H. Nguyen and A.W. Roscoe",
year = "2012",
journal = "IACR cryptology e-print archive",
url = "http://eprint.iacr.org/2012/429",
}
@article{roscoe2012xh3,
title = "User interactive Internet of things privacy preserved access control",
author = "Xin Huang, Rong Fu, Bangdao Chen, Tingting Zhang, A.W. Roscoe",
year = "2012",
journal = "ICITST",
url = "http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6470887",
}
@article{roscoe2012xh2,
title = "Bootstrapping body sensor networks using human controlled LED-camera channels",
author = "Xin Huang, Shangyuan Guo, Bangdao Chen, A.W. Roscoe",
year = "2012",
journal = "ICITST",
url = "http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6470845",
}
@article{roscoe2012SAT,
title = "SAT solving in CSP trace refinement",
author = "Hristina Palikareva and Joel Ouaknine and A.W. Roscoe",
year = "2012",
journal = "Science of Computer Programming",
url = "http://www.sciencedirect.com/science/article/pii/S0167642311001547",
volume = "77",
}
@article{roscoe2012xh1,
title = "Human Interactive Secure ID Management in Body Sensor Networks",
author = "Xin Huang, Xiao Ma, Bangdao Chen, Andrew Markham, Quinghua Wang, A.W. Roscoe",
year = "2012",
journal = "Journal of Networks",
url = "http://academypublisher.com/~academz3/ojs/index.php/jnw/article/view/jnw070914001406/5437",
volume = "7",
}
@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",
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",
}
@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{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",
}
@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{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",
}
@incollection{ouaknine2011static,
title = "Static livelock analysis in CSP",
author = "Ouaknine, J. and Palikareva, H. and Roscoe, A. and Worrell, J.",
year = "2011",
booktitle = "CONCUR 2011--Concurrency Theory",
isbn = "978-3-642-23216-9",
issn = "0302-9743",
pages = "389--403",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "http://www.springerlink.com/content/a14672716755020g/",
volume = "6901",
doi = "10.1007/978-3-642-23217-6_26",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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",
}
@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)",
}
@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",
}
@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{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{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",
}
@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}",
url = "http://www.cs.ox.ac.uk/people/bill.roscoe/publications/115.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",
}
@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{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",
}
@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",
}
@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{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{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{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",
}
@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",
}
@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",
}
@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{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{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",
}
@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{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",
}
@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{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",
}
@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{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",
}
@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",
}
@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}",
}
@inproceedings{Compiling,
title = "{Compiling Shared Variable Programs into CSP}",
author = "A. W. Roscoe",
year = "2001",
booktitle = "{Proceedings of PROGRESS workshop 2001}",
}
@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{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",
}
@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{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",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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{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{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",
}
@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{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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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",
}
@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{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",
}
@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",
}
@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://www.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",
}
@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{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",
}
@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",
}