Concurrency: Publications
Books
-
[1]
The theory and practice of concurrency
A. W. Roscoe
Prentice Hall. 1998.
The text book teaching material can be found at http://www.comlab.ox.ac.uk/publications/books/concurrency/
Details about The theory and practice of concurrency | BibTeX data for The theory and practice of concurrency | Download (pdf) of The theory and practice of concurrency
-
[2]
A Classical Mind: essays in Honour of C.A.R. Hoare
A. W. Roscoe, editor
Prentice−Hall. 1994.
Details about A Classical Mind: essays in Honour of C.A.R. Hoare | BibTeX data for A Classical Mind: essays in Honour of C.A.R. Hoare
Book chapters
-
[1]
Static Analysis to Enhance the Power of Model Checking for Concurrent Software
Edmund Clarke‚ Daniel Kroening and Thomas Reps
In Department of Defense Sponsored Information Security Research. Pages 349–360. Wiley. July, 2007.
Details about Static Analysis to Enhance the Power of Model Checking for Concurrent Software | BibTeX data for Static Analysis to Enhance the Power of Model Checking for Concurrent Software
-
[2]
The successes and failures of behavioural models
A. W. Roscoe‚ R. Forster and G.M. Reed
In Millennial Perspectives in Computer Science. Palgrave. 2000.
Details about The successes and failures of behavioural models | BibTeX data for The successes and failures of behavioural models | Download (pdf) of The successes and failures of behavioural models
-
[3]
A Case Study of the Formal Specification of a Parallel System using CSP
A. W. Roscoe and S. Kiyamura
In S. Noguchi and M. Ota, editors, Correct Models of Parallel Computing. IOS Press. 1997.
Details about A Case Study of the Formal Specification of a Parallel System using CSP | BibTeX data for A Case Study of the Formal Specification of a Parallel System using CSP
-
[4]
Model−checking CSP
A. W. Roscoe
In A Classical Mind: essays in Honour of C.A.R. Hoare. Chapter 21. Prentice−Hall. 1994.
Details about Model−checking CSP | BibTeX data for Model−checking CSP | Link to Model−checking CSP
Journal papers
-
[1]
On the expressiveness of CSP
A.W. Roscoe
2011.
Draft of February 2011‚ which is very different from previous draft (2008).
Details about On the expressiveness of CSP | BibTeX data for On the expressiveness of CSP | Download (pdf) of On the expressiveness of CSP
-
[2]
Specification of communicating processes: temporal logic versus refusals−based refinement
Gavin Lowe
In Formal Aspects of Computing. 2008.
Details about Specification of communicating processes: temporal logic versus refusals−based refinement | BibTeX data for Specification of communicating processes: temporal logic versus refusals−based refinement | Download (pdf) of Specification of communicating processes: temporal logic versus refusals−based refinement
-
[3]
Responsiveness and stable revivals
A. W. Roscoe‚ J. N. Reed and J. E. Sinclair
In Formal Aspects of Computing. Vol. 19. No. 3. August, 2007.
Details about Responsiveness and stable revivals | BibTeX data for Responsiveness and stable revivals | Download (pdf) of Responsiveness and stable revivals
-
[4]
Nets with Tokens Which Carry Data
A. W. Roscoe‚ Ranko Lazic‚ Tom Newcomb‚ Joel Ouaknine and James Worrell
In Springer LNCS 3349. 2007.
Details about Nets with Tokens Which Carry Data | BibTeX data for Nets with Tokens Which Carry Data | Download of Nets with Tokens Which Carry Data | Download (pdf) of Nets with Tokens Which Carry Data
-
[5]
Verification of Boolean Programs with Unbounded Thread Creation
Byron Cook‚ Daniel Kroening and Natasha Sharygina
In Theoretical Computer Science (TCS). Vol. 388. Pages 227–242. 2007.
Details about Verification of Boolean Programs with Unbounded Thread Creation | BibTeX data for Verification of Boolean Programs with Unbounded Thread Creation
-
[6]
On Timed Models and Full Abstraction
Gavin Lowe and Joël Ouaknine
In Electr. Notes Theor. Comput. Sci.. Vol. 155. Pages 497−519. 2006.
Details about On Timed Models and Full Abstraction | BibTeX data for On Timed Models and Full Abstraction | DOI (10.1016/j.entcs.2005.11.070) | Link to On Timed Models and Full Abstraction
-
[7]
A hierarchy of failures−based models: theory and application
Christie Bolton and Gavin Lowe
In Theoretical Computer Science. Vol. 330. No. 3. Pages 407−438. 2005.
Details about A hierarchy of failures−based models: theory and application | BibTeX data for A hierarchy of failures−based models: theory and application | DOI (10.1016/j.tcs.2004.10.004) | Link to A hierarchy of failures−based models: theory and application
-
[8]
A Hierarchy of Failures−Based Models
Christie Bolton and Gavin Lowe
In Electr. Notes Theor. Comput. Sci.. Vol. 96. Pages 129−152. 2004.
Details about A Hierarchy of Failures−Based Models | BibTeX data for A Hierarchy of Failures−Based Models | DOI (10.1016/j.entcs.2004.04.025)
-
[9]
Responsiveness of Interoperating Components
A. W. Roscoe‚ J. N. Reed and J. E. Sinclair
In Formal Aspects of Computing. Vol. 16. Pages 394–411. 2004.
Details about Responsiveness of Interoperating Components | BibTeX data for Responsiveness of Interoperating Components | Download (pdf) of Responsiveness of Interoperating Components
-
[10]
On Model Checking Data−independent Systems with Arrays without Reset
A. W. Roscoe‚ R. S. Lazic and T. C. Newcomb
In Theory and Practice of Logic Programming. Vol. 4. No. 5 & 6. Pages 659−693. 2004.
Details about On Model Checking Data−independent Systems with Arrays without Reset | BibTeX data for On Model Checking Data−independent Systems with Arrays without Reset | Download (pdf) of On Model Checking Data−independent Systems with Arrays without Reset
-
[11]
On the expressive power of CSP refinement
A. W. Roscoe
In Formal Aspects of Computing. Vol. 17 of 2. Pages 93–112. 2003.
Preliminary version in Proceedings of AVoCS03‚ Southampton University Technical Report‚ April 2003
Details about On the expressive power of CSP refinement | BibTeX data for On the expressive power of CSP refinement | Link to On the expressive power of CSP refinement
-
[12]
Proving security protocols with model checkers by data independence techniques
A. W. Roscoe and P.J. Broadfoot
In Journal of Computer Security. Vol. 7. 1999.
Details about Proving security protocols with model checkers by data independence techniques | BibTeX data for Proving security protocols with model checkers by data independence techniques | Download (pdf) of Proving security protocols with model checkers by data independence techniques
-
[13]
Probabilistic and Prioritized Models of Timed CSP
Gavin Lowe
In Theor. Comput. Sci.. Vol. 138. No. 2. Pages 315−352. 1995.
Details about Probabilistic and Prioritized Models of Timed CSP | BibTeX data for Probabilistic and Prioritized Models of Timed CSP | DOI (10.1016/0304-3975(94)00171-E) | Link to Probabilistic and Prioritized Models of Timed CSP
-
[14]
Scheduling−Oriented Models for Real−Time Systems
Gavin Lowe
In The Computer Journal. Vol. 38. No. 6. Pages 443−456. 1995.
Details about Scheduling−Oriented Models for Real−Time Systems | BibTeX data for Scheduling−Oriented Models for Real−Time Systems | Link to Scheduling−Oriented Models for Real−Time Systems
-
[15]
Refinement of Complex Systems: A Case Study
Gavin Lowe and Hussein Zedan
In The Computer Journal. Vol. 38. No. 10. Pages 785−800. 1995.
Details about Refinement of Complex Systems: A Case Study | BibTeX data for Refinement of Complex Systems: A Case Study | Link to Refinement of Complex Systems: A Case Study
-
[16]
Denotational semantics for occam2‚ Part 2
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Transputer Communications. Vol. 2 of 1. Pages 25–67. 1994.
Details about Denotational semantics for occam2‚ Part 2 | BibTeX data for Denotational semantics for occam2‚ Part 2
-
[17]
Denotational semantics for occam2‚ Part 1
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Transputer Communications. Vol. 1 of 2. Pages 65–91. 1994.
Details about Denotational semantics for occam2‚ Part 1 | BibTeX data for Denotational semantics for occam2‚ Part 1
-
[18]
Occam in the specification and verification of microprocessors
A. W. Roscoe
In 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
Details about Occam in the specification and verification of microprocessors | BibTeX data for Occam in the specification and verification of microprocessors | Link to Occam in the specification and verification of microprocessors
-
[19]
Analysing TM_FS: a study of nondeterminism in real−time concurrency
A. W. Roscoe and G.M. Reed
In Concurrency: Theory Language and Architecture. Vol. 491. 1991.
Details about Analysing TM_FS: a study of nondeterminism in real−time concurrency | BibTeX data for Analysing TM_FS: a study of nondeterminism in real−time concurrency | Link to Analysing TM_FS: a study of nondeterminism in real−time concurrency
-
[20]
A semantic model for occam II
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Proceedings of Transputing. Vol. 93. 1991.
Details about A semantic model for occam II | BibTeX data for A semantic model for occam II
-
[21]
Deadlock analysis in networks of communicating processes
A. W. Roscoe and S.D. Brookes
In Distributed Computing. No. 4. Pages 209–230. 1991.
Details about Deadlock analysis in networks of communicating processes | BibTeX data for Deadlock analysis in networks of communicating processes | Download (pdf) of Deadlock analysis in networks of communicating processes
-
[22]
A timed model for communicating sequential processes
A. W. Roscoe and G.M. Reed
In Theoretical Computer Science. Vol. 58. Pages 249–261. 1988.
Details about A timed model for communicating sequential processes | BibTeX data for A timed model for communicating sequential processes | Download (pdf) of A timed model for communicating sequential processes
-
[23]
The laws of occam programming
A. W. Roscoe and C.A.R. Hoare
In Theoretical Computer Science. Vol. 60. Pages 177–229. 1988.
Previously appeared as Oxford University Computing Laboratory Technical Report PRG−53‚ 1986.
Details about The laws of occam programming | BibTeX data for The laws of occam programming | Download (pdf) of The laws of occam programming
-
[24]
The pursuit of deadlock freedom
A. W. Roscoe and Naiem Dathi
In Information and Computation. Vol. 75. No. 3. Pages 289–327. December, 1987.
Details about The pursuit of deadlock freedom | BibTeX data for The pursuit of deadlock freedom | Link to The pursuit of deadlock freedom
-
[25]
A theory of communicating sequential processes
A. W. Roscoe‚ S.D. Brookes and C.A.R. Hoare
In Journal of the ACM. No. 3. Pages 560–599. July, 1984.
Details about A theory of communicating sequential processes | BibTeX data for A theory of communicating sequential processes | Download (pdf) of A theory of communicating sequential processes
Conference papers
-
[1]
Scalable Performance for Scala Message−Passing Concurrency
Andrew Bate
In Peter H. Welch‚ Frederick R. M. Barnes‚ Jan F. Broenink‚ Kevin Chalmers‚ Jan Bækgaard Pedersen and Adam T. Sampson, editors, Communicating Process Architectures 2013. Pages 113–132. November, 2013.
Details about Scalable Performance for Scala Message−Passing Concurrency | BibTeX data for Scalable Performance for Scala Message−Passing Concurrency | Download Bate13.pdf of Scalable Performance for Scala Message−Passing Concurrency | Download Bate13-slides.pdf of Scalable Performance for Scala Message−Passing Concurrency
-
[2]
A Debugger for Communicating Scala Objects
Andrew Bate and Gavin Lowe
In Peter H. Welch‚ Frederick R. M. Barnes‚ Kevin Chalmers‚ Jan Bækgaard Pedersen and Adam T. Sampson, editors, Communicating Process Architectures 2012. Pages 135–154. August, 2012.
Details about A Debugger for Communicating Scala Objects | BibTeX data for A Debugger for Communicating Scala Objects | Download (pdf) of A Debugger for Communicating Scala Objects
-
[3]
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.
Details about A representative function approach to symmetry exploitation for CSP refinement checking | BibTeX data for A representative function approach to symmetry exploitation for CSP refinement checking | Download (pdf) of A representative function approach to symmetry exploitation for CSP refinement checking
-
[4]
The three Platonic models of divergence−strict CSP
A.W. Roscoe
In Proceedings of ICTAC '08. 2008.
Details about The three Platonic models of divergence−strict CSP | BibTeX data for The three Platonic models of divergence−strict CSP | Download (pdf) of The three Platonic models of divergence−strict CSP
-
[5]
Formal verification of not fully symmetric systems using counter abstraction
Tomasz Mazur
In Proceedings of the MOdelling and VErifying Process (MOVEP'08). 2008.
Details about Formal verification of not fully symmetric systems using counter abstraction | BibTeX data for Formal verification of not fully symmetric systems using counter abstraction | Download (pdf) of Formal verification of not fully symmetric systems using counter abstraction
-
[6]
Model Checking Concurrent Linux Device Drivers
Thomas Witkowski‚ Nicolas Blanc‚ Georg Weissenbacher and Daniel Kroening
In 22nd IEEE International Conference on Automated Software Engineering (ASE). Pages 501–504. IEEE. 2007.
Details about Model Checking Concurrent Linux Device Drivers | BibTeX data for Model Checking Concurrent Linux Device Drivers | DOI (10.1145/1321631.1321719) | Link to Model Checking Concurrent Linux Device Drivers
-
[7]
SVA‚ a tool for analysing shared−variable programms
A. W. Roscoe and David Hopkins
In Proceedings of AVoCS 2007. Pages 177–183. 2007.
to appear
Details about SVA‚ a tool for analysing shared−variable programms | BibTeX data for SVA‚ a tool for analysing shared−variable programms | Download (pdf) of SVA‚ a tool for analysing shared−variable programms
-
[8]
Counter Abstraction in the CSP/FDR setting
Tomasz Mazur and Gavin Lowe
In Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS'07). 2007.
Details about Counter Abstraction in the CSP/FDR setting | BibTeX data for Counter Abstraction in the CSP/FDR setting | Download (pdf) of Counter Abstraction in the CSP/FDR setting
-
[9]
On CSP refinement tests that run multiple copies of a process
Gavin Lowe
2007.
Details about On CSP refinement tests that run multiple copies of a process | BibTeX data for On CSP refinement tests that run multiple copies of a process | Download (pdf) of On CSP refinement tests that run multiple copies of a process
-
[10]
Verifying Statemate Statecharts Using CSP and FDR
A. W. Roscoe and Zhenzhong Wu
In Proceedings of ICFEM 2006. 2006.
Details about Verifying Statemate Statecharts Using CSP and FDR | BibTeX data for Verifying Statemate Statecharts Using CSP and FDR | Download (pdf) of Verifying Statemate Statecharts Using CSP and FDR
-
[11]
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.
Details about A taxonomy of web services in CSP | BibTeX data for A taxonomy of web services in CSP | Download (pdf) of A taxonomy of web services in CSP
-
[12]
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
Details about Confluence thanks to extensional determinism | BibTeX data for Confluence thanks to extensional determinism | Download (pdf) of Confluence thanks to extensional determinism
-
[13]
Machine−Verifiable Responsiveness
A. W. Roscoe‚ J. N Reed and J. E Sinclair
In Proceedings of AVOCS 2005. 2005.
Details about Machine−Verifiable Responsiveness | BibTeX data for Machine−Verifiable Responsiveness | Download (pdf) of Machine−Verifiable Responsiveness
-
[14]
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.
Details about On Model checking data−independent systems with arrays with whole−array operations | BibTeX data for On Model checking data−independent systems with arrays with whole−array operations | Download (pdf) of On Model checking data−independent systems with arrays with whole−array operations
-
[15]
Seeing beyond divergence
A. W. Roscoe
In Communicating Sequential Processes‚ the first 25 years. No. 3525. Springer LNCS. 2005.
Details about Seeing beyond divergence | BibTeX data for Seeing beyond divergence | Download (pdf) of Seeing beyond divergence
-
[16]
On the Application of Counterexample−Guided Abstraction refinement and data independence to the parameterised model checking problem
Gavin Lowe
In Proceedings of the Third International Workshop on Automatic Verification of Infinite−State Systems‚ (AVIS 2004). 2004.
Details about On the Application of Counterexample−Guided Abstraction refinement and data independence to the parameterised model checking problem | BibTeX data for On the Application of Counterexample−Guided Abstraction refinement and data independence to the parameterised model checking problem | Link to On the Application of Counterexample−Guided Abstraction refinement and data independence to the parameterised model checking problem
-
[17]
Finitary refinement checks for infinitary specifications
A. W. Roscoe
In Proceedings of CPA 2004. June, 2004.
Details about Finitary refinement checks for infinitary specifications | BibTeX data for Finitary refinement checks for infinitary specifications | Download (pdf) of Finitary refinement checks for infinitary specifications
-
[18]
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.
Details about Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting | BibTeX data for Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting | Download (pdf) of Polymorphic Systems with Arrays‚ 2−Counter Machines and Multiset Rewriting
-
[19]
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.
Details about Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption | BibTeX data for Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption | Download (pdf) of Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
-
[20]
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
Details about Polymorphic systems with arrays: decidability and undecidability | BibTeX data for Polymorphic systems with arrays: decidability and undecidability | Download (pdf) of Polymorphic systems with arrays: decidability and undecidability
-
[21]
Watchdog transformations for property−oriented model checking
A. W. Roscoe‚ M.H. Goldsmith‚ N.Moffat‚ T. Whitworth and I. Zakiuddin
In Proceedings of FME 2003. 2003.
Details about Watchdog transformations for property−oriented model checking | BibTeX data for Watchdog transformations for property−oriented model checking | Download (pdf) of Watchdog transformations for property−oriented model checking
-
[22]
Capturing parallel attacks within the data independence framework
A. W. Roscoe and P. J. Broadfoot
In Proceedings of CSFW 15. IEEE Press. 2002.
Details about Capturing parallel attacks within the data independence framework | BibTeX data for Capturing parallel attacks within the data independence framework | Link to Capturing parallel attacks within the data independence framework
-
[23]
Internalising Agents in CSP Protocol Models
A. W. Roscoe and P. J. Broadfoot
In Proceedings of WITS 2002. 2002.
Extended Abstract
Details about Internalising Agents in CSP Protocol Models | BibTeX data for Internalising Agents in CSP Protocol Models | Link to Internalising Agents in CSP Protocol Models
-
[24]
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.
Details about On Model Checking Data−independent Systems with Arrays without Reset | BibTeX data for On Model Checking Data−independent Systems with Arrays without Reset | Link to On Model Checking Data−independent Systems with Arrays without Reset
-
[25]
What can you Decide about Resetable Arrays?
A. W. Roscoe and R. S. Lazic
In Proceedings of VCL 2001. 2001.
Details about What can you Decide about Resetable Arrays? | BibTeX data for What can you Decide about Resetable Arrays? | Link to What can you Decide about Resetable Arrays?
-
[26]
Compiling Shared Variable Programs into CSP
A. W. Roscoe
In Proceedings of PROGRESS workshop 2001. 2001.
Details about Compiling Shared Variable Programs into CSP | BibTeX data for Compiling Shared Variable Programs into CSP | Download (pdf) of Compiling Shared Variable Programs into CSP
-
[27]
Automating Data Independence
Philippa J. Broadfoot‚ Gavin Lowe and A. W. Roscoe
In Frédéric Cuppens‚ Yves Deswarte‚ Dieter Gollmann and Michael Waidner, editors, Computer Security − ESORICS 2000‚ 6th European Symposium on Research in Computer Security‚ Toulouse‚ France‚ October 4−6‚ 2000‚ Proceedings. Vol. 1895 of Lecture Notes in Computer Science. Pages 175−190. Springer. 2000.
Details about Automating Data Independence | BibTeX data for Automating Data Independence | DOI (10.1007/10722599_11) | Link to Automating Data Independence
-
[28]
Automating Data Independence
A. W. Roscoe‚ P.J. Broadfoot and G. Lowe
In Proceedings of ESORICS2000. Vol. 1895. LNCS. 2000.
Details about Automating Data Independence | BibTeX data for Automating Data Independence | Download (pdf) of Automating Data Independence
-
[29]
Data independent induction over structured networks
A. W. Roscoe and S.J. Creese
In Proceedings of PDPTA2000. 2000.
Details about Data independent induction over structured networks | BibTeX data for Data independent induction over structured networks | Link to Data independent induction over structured networks
-
[30]
Data independence with predicate symbols
A. W. Roscoe and R.S. Lazic
In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99). Vol. I. CSREA Press. 1999.
Details about Data independence with predicate symbols | BibTeX data for Data independence with predicate symbols | Link to Data independence with predicate symbols
-
[31]
Formal Verification of Arbitrary Network Topologies
A. W. Roscoe and S.J. Creese
In Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99). Vol. II. CSREA Press. 1999.
Details about Formal Verification of Arbitrary Network Topologies | BibTeX data for Formal Verification of Arbitrary Network Topologies | Download (pdf) of Formal Verification of Arbitrary Network Topologies
-
[32]
Proving security protocols with model checkers by data independence techniques
A. W. Roscoe
In Proceedings of CSFW 1998. IEEE Press. 1998.
Details about Proving security protocols with model checkers by data independence techniques | BibTeX data for Proving security protocols with model checkers by data independence techniques | Download (pdf) of Proving security protocols with model checkers by data independence techniques
-
[33]
Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays
A. W. Roscoe and R. Lazic
In Proceedings of INFINITY'98. July, 1998.
extended version as Oxford University Computing Laboratory TR−2−98.
Details about Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays | BibTeX data for Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays | Link to Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays
-
[34]
Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock
A. W. Roscoe‚ D.M.Jackson P.H.B. Gardiner M.H. Goldsmith J.R. Hulance and J.B. Scattergood
In Proceedings of TACAS 1995. BRICS. 1995.
also revised in a version of these proceedings published by LNCS
Details about Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock | BibTeX data for Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock | Download (pdf) of Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock
-
[35]
Developing and verifying protocols in CSP
A. W. Roscoe
In Proceedings of Mierlo workshop on protocols. TU Eindhoven. 1993.
Details about Developing and verifying protocols in CSP | BibTeX data for Developing and verifying protocols in CSP
-
[36]
Timed CSP: theory and practice
A. W. Roscoe‚ J.Davies‚ D.Jackson‚ G.M.Reed‚ J.Reed and S.A. Schneider
In Proceedings of REX Workshop. Vol. 600. LNCS. 1992.
Details about Timed CSP: theory and practice | BibTeX data for Timed CSP: theory and practice
-
[37]
CSP and timewise refinement
A. W. Roscoe‚ G. M. Reed and S. A. Schneider
In Proceedings of the BCS−FACS Refinement Workshop. LNCS. 1991.
Details about CSP and timewise refinement | BibTeX data for CSP and timewise refinement
-
[38]
Unbounded nondeterminism in CSP
A. W. Roscoe and G.Barrett
In Proceedings of MFPS89. No. 298. Springer. 1989.
Details about Unbounded nondeterminism in CSP | BibTeX data for Unbounded nondeterminism in CSP | Download (pdf) of Unbounded nondeterminism in CSP
-
[39]
Transforming occam programs
A. W. Roscoe and M.H. Goldsmith
In The Design and Application of Parallel Digital Processors. No. 298. 1988.
Details about Transforming occam programs | BibTeX data for Transforming occam programs | Download (pdf) of Transforming occam programs
-
[40]
Metric spaces as models for real−time concurrency
A. W. Roscoe and 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.
Details about Metric spaces as models for real−time concurrency | BibTeX data for Metric spaces as models for real−time concurrency | Download (pdf) of Metric spaces as models for real−time concurrency
-
[41]
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..
Details about Routing messages through networks: an exercise in deadlock avoidance | BibTeX data for Routing messages through networks: an exercise in deadlock avoidance | Link to Routing messages through networks: an exercise in deadlock avoidance
-
[42]
A timed model for communicating sequential processes
A. W. Roscoe and G.M. Reed
In Proc.ICALP 86. No. 226. Pages 314–323. Springer. 1986.
Details about A timed model for communicating sequential processes | BibTeX data for A timed model for communicating sequential processes | Download (pdf) of A timed model for communicating sequential processes
-
[43]
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.
Details about Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification | BibTeX data for Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification | Download (pdf) of Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification
-
[44]
Denotational semantics for occam
A. W. Roscoe
In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 306–329. Springer. 1985.
Details about Denotational semantics for occam | BibTeX data for Denotational semantics for occam | Download (pdf) of Denotational semantics for occam
-
[45]
Deadlock analysis in networks of communicating processes
A. W. Roscoe and 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.
Details about Deadlock analysis in networks of communicating processes | BibTeX data for Deadlock analysis in networks of communicating processes
-
[46]
An improved failures model for communicating processes
A. W. Roscoe and S.D. Brookes
In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 281–305. Springer. 1985.
Details about An improved failures model for communicating processes | BibTeX data for An improved failures model for communicating processes | Download (pdf) of An improved failures model for communicating processes
-
[47]
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.
Details about A CSP solution to the trains problem | BibTeX data for A CSP solution to the trains problem | Download (pdf) of A CSP solution to the trains problem
-
[48]
Programs as executable predicates
A. W. Roscoe and C.A.R. Hoare
In Proceedings of FGCS84 (ICOT‚ editors). Pages 220–228. 1984.
Details about Programs as executable predicates | BibTeX data for Programs as executable predicates | Download (pdf) of Programs as executable predicates
Technical reports
-
[1]
A taxonomy of web services using CSP
Lee Momtahan‚ Andrew Martin and A. W. Roscoe
No. RR−04−22. Oxford University Computing Laboratory. October, 2004.
Details about A taxonomy of web services using CSP | BibTeX data for A taxonomy of web services using CSP | Download (ps) of A taxonomy of web services using CSP
-
[2]
Bisimulation and refinement reconciled
A. W. Roscoe‚ C.A.R. Hoare‚ C. Fournet‚ P.H.B. Gardiner‚ R. Milner‚ S.Rajamani and J. Rehof
Microsoft. 2003.
Details about Bisimulation and refinement reconciled | BibTeX data for Bisimulation and refinement reconciled
-
[3]
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. Oxford University Computing Laboratory. April, 2003.
Details about Translating CSP trace refinement to UNITY unreachability : a study in data independence | BibTeX data for Translating CSP trace refinement to UNITY unreachability : a study in data independence | Download (ps.gz) of Translating CSP trace refinement to UNITY unreachability : a study in data independence | Link to Translating CSP trace refinement to UNITY unreachability : a study in data independence
-
[4]
TTP: A case study in combining induction and data independence
A. W. Roscoe and S.J. Creese
No. PRG−TR−1−99. Oxford University Computing Laboratory. 1999.
Details about TTP: A case study in combining induction and data independence | BibTeX data for TTP: A case study in combining induction and data independence | Link to TTP: A case study in combining induction and data independence
-
[5]
The timed failures−stability model for Timed CSP
A. W. Roscoe and G.M. Reed
No. PRG−119. Oxford University Computing Laboratory. 1996.
also appeared in Theoretical Computer Science‚ Vol 211 (1999)
Details about The timed failures−stability model for Timed CSP | BibTeX data for The timed failures−stability model for Timed CSP | Download (pdf) of The timed failures−stability model for Timed CSP
-
[6]
Denotational semantics for occam II
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
No. PRG−108. Oxford University Computing Laboratory. 1993.
Details about Denotational semantics for occam II | BibTeX data for Denotational semantics for occam II | Download (pdf) of Denotational semantics for occam II
-
[7]
Maintaining consistency in distributed databases
A. W. Roscoe
No. PRG−87. Oxford University Computing Laboratory. 1990.
Details about Maintaining consistency in distributed databases | BibTeX data for Maintaining consistency in distributed databases | Link to Maintaining consistency in distributed databases
-
[8]
Communication and correctness in Timed CSP
A. W. Roscoe‚ S.A. Schneider‚ J.W. Davies‚ D.M. Jackson and G.M. Reed
Esprit SPEC project. 1990.
Details about Communication and correctness in Timed CSP | BibTeX data for Communication and correctness in Timed CSP
-
[9]
A temporal logic for Timed CSP
D.M. Jackson‚ J.W. Davies‚ G.M. Reed and S.A. Schneider
Esprit SPEC project. 1990.
Details about A temporal logic for Timed CSP | BibTeX data for A temporal logic for Timed CSP
-
[10]
Unbounded nondeterminism in CSP
A. W. Roscoe
No. PRG−67. 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)
Details about Unbounded nondeterminism in CSP | BibTeX data for Unbounded nondeterminism in CSP | Link to Unbounded nondeterminism in CSP
-
[11]
An alternative order for the failures model
A. W. Roscoe
No. PRG−67. Oxford University Computing Laboratory. July, 1988.
in Two papers on CSP‚ Also appeared in Journal of Logic and Computation 2‚ 5 pp557−577
Details about An alternative order for the failures model | BibTeX data for An alternative order for the failures model | Link to An alternative order for the failures model
-
[12]
An Operational Semantics for CSP
A. W. Roscoe‚ S. D. Brookes and D. J. Walker
Oxford University Computing Laboratory. 1986.
Details about An Operational Semantics for CSP | BibTeX data for An Operational Semantics for CSP | Link to An Operational Semantics for CSP
-
[13]
A theory of communicating sequential processes
A. W. Roscoe‚ S.D. Brookes and C. A. R. Hoare
No. PRG−16. Oxford University Computing Laboratory. May, 1981.
Details about A theory of communicating sequential processes | BibTeX data for A theory of communicating sequential processes | Download (pdf) of A theory of communicating sequential processes
Theses
-
[1]
Probabilities and Priorities in Timed CSP
Gavin Lowe
PhD Thesis , type= DPhil thesis. Oxford University Computing Laboratory. 1993.
Details about Probabilities and Priorities in Timed CSP | BibTeX data for Probabilities and Priorities in Timed CSP | Link to Probabilities and Priorities in Timed CSP
-
[2]
A mathematical theory of communicating processes
A. W. Roscoe
PhD Thesis , type= D. Phil. Thesis. Oxford University. 1982.
Please note this is a 270 page‚ 118 Mb scanned file and will take some time to download.
Details about A mathematical theory of communicating processes | BibTeX data for A mathematical theory of communicating processes | Download (pdf) of A mathematical theory of communicating processes
Miscellaneous
-
[1]
Revivals‚stuckness and the hierarchy of CSP Models
A. W. Roscoe
December, 2008.
to appear (revision of 2005 and 2007 drafts)
Details about Revivals‚stuckness and the hierarchy of CSP Models | BibTeX data for Revivals‚stuckness and the hierarchy of CSP Models | Download (pdf) of Revivals‚stuckness and the hierarchy of CSP Models
-
[2]
Modelling unbounded parallel sessions of security protocols in CSP
A. W. Roscoe and E. Kleiner
2006.
Details about Modelling unbounded parallel sessions of security protocols in CSP | BibTeX data for Modelling unbounded parallel sessions of security protocols in CSP | Download (pdf) of Modelling unbounded parallel sessions of security protocols in CSP
-
[3]
The pursuit of buffer tolerance
A. W. Roscoe
May, 2005.
unpublished draft
Details about The pursuit of buffer tolerance | BibTeX data for The pursuit of buffer tolerance | Download (pdf) of The pursuit of buffer tolerance
-
[4]
Compiling Statemate Statecharts into CSP and verifying them using FDR
A. W. Roscoe
January, 2003.
Extended Abstract
Details about Compiling Statemate Statecharts into CSP and verifying them using FDR | BibTeX data for Compiling Statemate Statecharts into CSP and verifying them using FDR | Link to Compiling Statemate Statecharts into CSP and verifying them using FDR