OXFORD UNIVERSITY COMPUTING LABORATORY

Bill Roscoe: Publications

personal ordering | bibtex

[0]

Notes on Domain Theory

A. W. Roscoe

1989.

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".

[1]

A theory of communicating sequential processes

A. W. Roscoe, S.D. Brookes and C. A. R. Hoare

No. {PRG-16}, Technical Report, Oxford University Computing Laboratory. May 1981.

[2]

A mathematical theory of communicating processes

A. W. Roscoe

PhD Thesis, Oxford University. 1982.

Please note this is a 270 page, 118 Mb scanned file and will take some time to download.

[3]

Criteria for metrisability

A. W. Roscoe, P.J. Collins

Proc. Amer. Math. Soc. No. 90, pages 631-640. 1984.

[4]

A theory of communicating sequential processes

A. W. Roscoe, S.D. Brookes and C.A.R. Hoare

Journal of the ACM, No. 3, pages 560—599. July 1984.

[5]

Programs as executable predicates

A. W. Roscoe, C.A.R. Hoare

In Proceedings of FGCS84 (ICOT, editors) pages 220—228. 1984.

[6]

Continuous analogues of axiomatised digital surfaces

A. W. Roscoe, T.Y. Kong

Computer Vision, Graphics and Image Processing, No. 29, pages 60—86. January 1985.

[7]

A lattice of conditions on topological spaces

A. W. Roscoe et al.

Proc. Amer. Math. Soc. No. 94, pages 487—496. July 1985.

[8]

Proceedings of the Pittsburgh seminar on concurrency

A. W. Roscoe, S.D. Brookes and G. Winskel, editors

No. 197, Springer. 1985.

[9]

An improved failures model for communicating processes

A. W. Roscoe, S.D. Brookes

In Proceedings of the Pittsburgh seminar on concurrency No. 197, pages 281—305. Springer, 1985.

[10]

Denotational semantics for occam

A. W. Roscoe

In Proceedings of the Pittsburgh seminar on concurrency No. 197, pages 306—329. Springer, 1985.

[11]

Deadlock analysis in networks of communicating processes

A. W. Roscoe, S.D. Brookes

In K.R. Apt, editor, Logics and Models of Concurrent Systems Vol. 13 of NATO ASI series F, pages 305—324. Springer, 1985.

[12]

Characterisations of simply-connected finite polyhedra in 3-space

A. W. Roscoe, T.Y. Kong

Bull. London Math. Soc. No. 17, pages 575—578. November 1985.

[13]

A theory of binary digital pictures

A. W. Roscoe, T.Y. Kong

Computer Vision, Graphics and Image Processing, No. 32, pages 221—243. November 1985.

[14]

Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification

A. W. Roscoe

In B.T. Denvir et al, editor, The Analysis of Concurrent Systems No. 207, pages 103—109. Springer, 1985.

[15]

A CSP solution to the trains problem

A. W. Roscoe

In B.T. Denvir et al, editor, The Analysis of Concurrent Systems No. 207, pages 384—388. Springer, 1985.

[16]

Local symmetry and triangle laws are sufficient for metrisability

A. W. Roscoe, P.J. Collins

Colloquia Mathematica Societatis Janos Bolyai 41, pages 177—181. 1985.

[17]

A timed model for communicating sequential processes

A. W. Roscoe, G.M. Reed

Theoretical Computer Science, Vol. 58, pages 249—261. 1988.

[18]

The pursuit of deadlock freedom

A. W. Roscoe, Naiem Dathi

Information and Computation, Vol. 75, No. 3, pages 289—327. December 1987.

[19]

Metric spaces as models for real-time concurrency

A. W. Roscoe, G.M. Reed

In Main et al, editor, Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans, 1987) No. 298, pages 331—343. Springer, 1988.

[20]

Laws of programming

A. W. Roscoe et al.

Communications of the ACM, Vol. 30, No. 8, pages 672—686. August 1987.

Previously appeared as Oxford University Computing Laboratory Technical Report PRG-42.

[21]

Routing messages through networks: an exercise in deadlock avoidance

A. W. Roscoe

In Muntean et al., editor, Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting Amsterdam. 1987. IOS B.V.

[22]

Transforming occam programs

A. W. Roscoe, M.H. Goldsmith

In The Design and Application of Parallel Digital Processors No. 298, 1988.

[23]

A timed model for communicating sequential processes

A. W. Roscoe, G.M. Reed

In Proc.ICALP 86 No. 226, pages 314—323. Springer, 1986.

[24]

The laws of occam programming

A. W. Roscoe, C.A.R. Hoare

Theoretical Computer Science, Vol. 60, pages 177—229. 1988.

Previously appeared as Oxford University Computing Laboratory Technical Report PRG-53, 1986.

[25]

The decomposition of a rectangle into rectangles of minimal perimeter

A. W. Roscoe, T.Y. Kong and D.M. Mount

No. {CAR-TR-169}, Technical Report, University of Maryland Center for Automation Research. 1986.

Also SIAM Journal of Computing 17, 6 pp1215-1231.

[26]

An Operational Semantics for CSP

A. W. Roscoe, S. D. Brookes and D. J. Walker

Technical Report, Oxford University Computing Laboratory. 1986.

[27]

An alternative order for the failures model

A. W. Roscoe

No. PRG-67, Technical Report, Oxford University Computing Laboratory. July 1988.

in Two papers on CSP, Also appeared in Journal of Logic and Computation 2, 5 pp557-577.

[28]

Unbounded nondeterminism in CSP

A. W. Roscoe

No. PRG-67, Technical Report, Oxford University Computing Laboratory. July 1988.

in Two papers on CSP, Also appeared in Journal of Logic and Computation, Vol 3, No 2 pp131-172 (1993).

[29]

Unbounded nondeterminism in CSP

A. W. Roscoe, G.Barrett

In Proceedings of MFPS89 No. 298, Springer, 1989.

[30]

Deadlock analysis in networks of communicating processes

A. W. Roscoe, S.D. Brookes

Distributed Computing, No. 4, pages 209—230. 1991.

[31]

A lattice of conditions on topological spaces II

A. W. Roscoe et al.

Fundamenta Mathematicae, No. 138, pages 69—81. 1991.

[32]

The point-countable base problem

A. W. Rosoce, P.J. Collins and G.M. Reed

In G.M. Reed, J. van Mill, editors, Problems in Topology Elsevier. 1990.

[33]

Maintaining consistency in distributed databases

A. W. Roscoe

No. {PRG-87}, Technical Report, Oxford University Computing Laboratory. 1990.

[34]

Communication and correctness in Timed CSP

A. W. Roscoe et al.

Technical Report, Esprit SPEC project. 1990.

[35]

A temporal logic for Timed CSP

D.M. Jackson et al.

Technical Report, Esprit SPEC project. 1990.

[36]

Topology, computer science and the mathematics of convergence

A. W. Roscoe

In G.M. Reed, A. W. Roscoe and R.F. Wachter, editors, Topology and Category Theory in Computer Science OUP. 1991.

[37]

Topology and category theory in computer science

A. W. Roscoe, G.M. Reed and R.F. Wachter, editors

OUP. 1991.

proceedings of a special session at the 1989 Oxford Topology Conference.

[38]

Analysing TM_FS: a study of nondeterminism in real-time concurrency

A. W. Roscoe, G.M. Reed

Concurrency: Theory Language and Architecture, Vol. 491. 1991.

[39]

CSP and timewise refinement

A. W. Roscoe, G. M. Reed and S. A. Schneider

In Proceedings of the BCS-FACS Refinement Workshop LNCS, 1991.

[40]

Star covering properties

A. W. Roscoe et al.

Topology and its Applications, Vol. 39, pages 71-103. 1991.

[41]

Formal methods in the development of the H1 Transputer

A. W. Roscoe et al.

In Proceedings of Transputing 91 IOS, 1991.

[42]

Concepts of digital topology

A. W. Roscoe, T.Y. Kong

Topology and its applications, Vol. 46, pages 219—262. 1992.

[43]

Timed CSP: theory and practice

A. W. Roscoe et al.

In Proceedings of REX Workshop Vol. 600. LNCS, 1992.

[44]

Acyclic monotone normality

A. W. Roscoe, P. Moody

Topology and its Applications, Vol. 47, pages 53-67. 1992.

[45]

Occam in the specification and verification of microprocessors

A. W. Roscoe

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

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

[46]

A semantic model for occam II

A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott

Proceedings of Transputing, Vol. 93. 1991.

[47]

Denotational semantics for occam II

A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott

No. PRG-108, Technical Report, Oxford University Computing Laboratory. 1993.

[48]

Developing and verifying protocols in CSP

A. W. Roscoe

In Proceedings of Mierlo workshop on protocols TU Eindhoven, 1993.

[49]

Fixed points without completeness

A. W. Roscoe, M.W. Mislove and S.A. Schneider

Theoretical Computer Science, Vol. 138, chapter 2, pages 273—314. 1993.

[50]

Model-checking CSP

A. W. Roscoe

In A Classical Mind: essays in Honour of C.A.R. Hoare chapter 21, Prentice-Hall. 1994.

[51]

A Classical Mind: essays in Honour of C.A.R. Hoare

A. W. Roscoe, editor

Prentice-Hall. 1994.

[52]

Denotational semantics for occam2, Part 1

A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott

Transputer Communications, Vol. 1 of 2, pages 65—91. 1994.

[53]

Denotational semantics for occam2, Part 2

A. W. Roscoe, M.H. Goldsmith and B.G.O. Scott

Transputer Communications, Vol. 2 of 1, pages 25—67. 1994.

[54]

Non-interference through determinism

A. W. Roscoe, J.C.P. Woodcock and L. Wulf

In Proceedings of ESORICS 94 1994.

[55]

Non-interference through determinism

A. W. Roscoe, J.C.P. Woodcock and L. Wulf

Journal of Computer Security, Vol. 4 of 1, pages 27—54. 1996.

revised version of above.

[56]

CSP and determinism in security modelling

1996

In Proceedings of 1995 IEEE Symposium on Security and Privacy IEEE Computer Society Press, 1996.

[57]

Composing and decomposing systems under security properties

A. W. Roscoe, L. Wulf

In Proceedings of 1995 IEEE Computer Security Foundations Workshop IEEE Computer Society Press, 1995.

[58]

Modelling and verifying key-exchange protocols using CSP and FDR

A. W. Roscoe

In Proceedings of 1995 IEEE Computer Security Foundations Workshop IEEE Computer Society Press, 1995.

[59]

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

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

In Proceedings of TACAS 1995 BRICS, 1995.

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

[60]

The timed failures-stability model for Timed CSP

A. W. Roscoe, G.M. Reed

No. {PRG-119}, Technical Report, Oxford University Computing Laboratory. 1996.

also appeared in Theoretical Computer Science, Vol 211 (1999).

[61]

Intensional specifications of security protocols

A. W. Roscoe

In Proceedings of 1996 IEEE Computer Security Foundations Workshop IEEE Computer Society Press, 1996.

[62]

On transition systems and non-well-founded sets

A. W. Roscoe, R.S. Lazic

Annals of the New York Academiy of Sciences, Vol. 806. 1996.

[63]

The perfect spy for model-checking crypto-protocols

A. W. Roscoe, M.H. Goldsmith

In Proceedings of DIMACS workshop on the design and formal verification of crypto-protocols 1997.

http://dimacs.rutgers.edu/workshops/program2/program.html

[64]

A Case Study of the Formal Specification of a Parallel System using CSP

A. W. Roscoe, S. Kiyamura

In S. Noguchi, M. Ota, editors, Correct Models of Parallel Computing IOS Press. 1997.

[65]

Using CSP to detect errors in the TMN protocol

A. W. Roscoe, G. Lowe

Technical Report, University of Leicester. 1996.

and IEEE transactions on Software Engineering Vol 23 (1997).

[66]

Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays

A. W. Roscoe, R. Lazic

In Proceedings of INFINITY'98 July 1998.

extended version as Oxford University Computing Laboratory TR-2-98.

[67]

Proving security protocols with model checkers by data independence techniques

A. W. Roscoe

In Proceedings of CSFW 1998 IEEE Press, 1998.

[68]

The theory and practice of concurrency

A. W. Roscoe

Prentice Hall. 1998.

[69]

What is intransitive noninterference?

A. W. Roscoe, M.H. Goldsmith

In Proceedings of CSFW 1999 IEEE Press, 1999.

[70]

Proving security protocols with model checkers by data independence techniques

A. W. Roscoe, P.J. Broadfoot

Journal of Computer Security, Vol. 7. 1999.

[71]

Data independence with predicate symbols

A. W. Roscoe, R.S. Lazic

In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99) Vol. I. CSREA Press, 1999.

[72]

Verifying an infinite family of inductions simultaneously using data independence and FDR

A. W. Roscoe, S.J. Creese

In 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) Kluwer Academic Publishers, 1999.

[73]

Formal Verification of Arbitrary Network Topologies

A. W. Roscoe, S.J. Creese

In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99) Vol. II. CSREA Press, 1999.

[74]

TTP: A case study in combining induction and data independence

A. W. Roscoe, S.J. Creese

No. {PRG-TR-1-99}, Technical Report, Oxford University Computing Laboratory. 1999.

[75]

Data independent induction over structured networks

A. W. Roscoe, S.J. Creese

In Proceedings of PDPTA2000 2000.

[76]

Automating Data Independence

A. W. Roscoe, P.J. Broadfoot and G. Lowe

In Proceedings of ESORICS2000 Vol. 1895. LNCS, 2000.

[77]

Millennial Perspectives in Computer Science

A. W. Roscoe, J. Davies and J. Woodcock, editors

Palgrave. 2000.

[78]

The successes and failures of behavioural models

A. W. Roscoe, R. Forster and G.M. Reed

In Millennial Perspectives in Computer Science Palgrave. 2000.

[79]

The Modelling and Analysis of Security Protocols

A. W. Roscoe et al.

Addison-Wesley. 2001.

[81]

What can you Decide about Resetable Arrays?

A. W. Roscoe, R. S. Lazic

In Proceedings of VCL 2001 2001.

[82]

Compiling Shared Variable Programs into CSP

A. W. Roscoe

In Proceedings of PROGRESS workshop 2001 2001.

[83]

Internalising Agents in CSP Protocol Models

A. W. Roscoe, P. J. Broadfoot

In Proceedings of WITS 2002 2002.

Extended Abstract.

[84]

Capturing parallel attacks within the data independence framework

A. W. Roscoe, P. J. Broadfoot

In Proceedings of CSFW 15 IEEE Press, 2002.

[85]

On Model Checking Data-independent Systems with Arrays without Reset

A. W. Roscoe, R. S. Lazic and T. C. Newcomb

In Proceedings of VCL 2001 2001.

[85]

On Model Checking Data-independent Systems with Arrays without Reset

A. W. Roscoe, R. S. Lazic and T. C. Newcomb

Theory and Practice of Logic Programming, Vol. 4, No. 5 & 6, pages 659-693. 2004.

[86]

Embedding agents within the intruder to detect parallel attacks

A. W. Roscoe, P.J. Broadfoot

Journal of Computer Security, Vol. 12, No. 3-4, pages 379-408. 2004.

[87]

Authentication in pervasive computing

A. W. Roscoe et al.

In Proceedings of First International Conference on Pervasive Computing (March 2003) LNCS, 2003.

[88]

Bisimulation and refinement reconciled

A. W. Roscoe et al.

Technical Report, Microsoft. 2003.

[89]

On the expressive power of CSP refinement

A. W. Roscoe

Formal Aspects of Computing, Vol. 17 of 2, pages 93—112. 2003.

Preliminary version in Proceedings of AVoCS03, Southampton University Technical Report, April 2003.

[90]

Polymorphic systems with arrays: decidability and undecidability

A. W. Roscoe, R. S. Lazic and T. C. Newcomb

In Proceedings of South-East Europe Workshop on Formal Methods August 2003.

Extended abstract.

[91]

Watchdog transformations for property-oriented model checking

A. W. Roscoe et al.

In Proceedings of FME 2003 2003.

[92]

The attacker in ubiquitous computing environments: formalising the threat model

A. W. Roscoe et al.

In Proceedings of FAST 2003, Pisa 2003.

[93]

Translating CSP trace refinement to UNITY unreachability : a study in data independence

A. W. Roscoe, Xu Wang and R.S. Lazic

No. RR-03-08, Technical Report, Oxford University Computing Laboratory. 2003.

[94]

Compiling Statemate Statecharts into CSP and verifying them using FDR

A. W. Roscoe

January 2003.

Extended Abstract.

[95]

Seeing beyond divergence

A. W. Roscoe

In Communicating Sequential Processes, the first 25 years No. 3525, Springer LNCS, 2005.

[96]

Finitary refinement checks for infinitary specifications

A. W. Roscoe

In Proceedings of CPA 2004 June 2004.

[97]

Research directions for trust and security in human-centric computing

A. W. Roscoe et al.

In Proceedings of SPPC 2004 2004.

[98]

Responsiveness of Interoperating Components

A. W. Roscoe, J. N. Reed and J. E. Sinclair

Formal Aspects of Computing, Vol. 16, pages 394—411. 2004.

[99]

Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption

A. W. Roscoe, Xu Wang and R. S. Lazic

In Proceedings of IFM 2004 Vol. 2999. Springer LNCS, 2004.

[100]

Web Services Security: a preliminary study using Casper and FDR

A. W. Roscoe, E. Kleiner

In Proceedings of Automated Reasoning for Security Protocol Analysis (ARSPA 04) 2004.

[101]

Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting

A. W. Roscoe, R. S. Lazic and Tom Newcomb

In Proceedings of INFINITY 2004 2004.

[102]

On Model checking data-independent systems with arrays with whole-array operations

A. W. Roscoe, R. S. Lazic and Tom Newcomb

In Communicating Sequential Processes No. 3525, Springer LNCS, 2005.

[103]

Exploiting Empirical Engagement in Authentication Protocol Design

A. W. Roscoe et al.

In Proceedings of SPPC 2005 2005.

[104]

On the relationship between Web Services Security and traditional protocols

A. W. Roscoe, Eldar Kleiner

In Proceedings of MFPS 2005 2005.

To appear.

[105]

Revivals,stuckness and the hierarchy of CSP Models

A. W. Roscoe

December 2008.

to appear (revision of 2005 and 2007 drafts).

[106]

The pursuit of buffer tolerance

A. W. Roscoe

May 2005.

unpublished draft.

[107]

Confluence thanks to extensional determinism

A. W. Roscoe

In Proceedings of Bertinoro meeting on Concurrency, BRICS 2005 May 2005.

Revised version, publication reference ENTCS 1336, 2006.

[108]

Security and trust for ubiquitous communication

A. W. Roscoe et al.

In ITU WSIS Thematic Meeting on Cybersecurity, Geneva, Switzerland June 2005.

[109]

Machine-Verifiable Responsiveness

A. W. Roscoe, J. N Reed and J. E Sinclair

In Proceedings of AVOCS 2005 2005.

[110]

Extending noninterference properties to the timed world

A. W. Roscoe, Jian Huang

In Proceedings of SAC 2006 2006.

to appear.

[111]

Bootstrapping Multi-Party Ad-Hoc Security

A. W. Roscoe et al.

In Proceedings of SAC 2006 2006.

to appear.

[112]

A taxonomy of web services using CSP

Lee Momtahan, Andrew Martin and A. W. Roscoe

No. RR-04-22, Technical Report, Oxford University Computing Laboratory. October 2004.

[112]

A taxonomy of web services in CSP

A. W. Roscoe, A. Martin and L. Momtahan

In Proceedings of Web Languages and Formal Methods 2005 2005.

[113]

Human-centred computer security

A. W. Roscoe

2006.

Unpublished draft.

[114]

Modelling unbounded parallel sessions of security protocols in CSP

A. W. Roscoe, E. Kleiner

2006.

[115]

Verifying Statemate Statecharts Using CSP and FDR

A. W. Roscoe, Zhenzhong Wu

In Proceedings of ICFEM 2006 2006.

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

[116]

Efficient group authentication protocols based on human interaction

A. W. Roscoe, L. H. Nguyen

In Proceedings of ARSPA 2006 2006.

[117]

Responsiveness and stable revivals

A. W. Roscoe, J. N. Reed and J. E. Sinclair

Formal Aspects of Computing, Vol. 19, No. 3, August 2007.

[118]

Nets with Tokens Which Carry Data

A. W. Roscoe et al.

Springer LNCS 3349, 2007.

[119]

SVA, a tool for analysing shared-variable programms

A. W. Roscoe, David Hopkins

In Proceedings of AVoCS 2007 pages 177—183. 2007.

to appear.

[120]

Authenticating ad hoc networks by comparison of short digests

A. W. Roscoe, L. H. Nguyen

Information and Computation, Vol. 206, pages 250-271. 2008.

[121]

The three Platonic models of divergence-strict CSP

A.W. Roscoe

In Proceedings of ICTAC '08 2008.

[122]

Separating two roles of hashing in one-way message authentication

L.H. Nguyen, A.W. Roscoe

In Proceedings of FCS-ARSPA-WITS 2008.

(This version is extended by appendices not present in proceedings.).

[124]

A representative function approach to symmetry exploitation for CSP refinement checking

N Moffat, M.H. Goldsmith and A.W. Roscoe

In Proceedings of IFCEM 2008 2008.

[125]

On the expressiveness of CSP

A.W. Roscoe

2008.

Draft of October 23, 2008.

Random Image
Random Image
Random Image