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", }