Concurrency: Publications
|
[1] |
A Debugger for Communicating Scala Objects Andrew Bate and Gavin Lowe In Peter H. Welch‚ Frederick R. M. Barnes‚ Kevin Chalmers‚ Jan Baekgaard Pedersen and Adam T. Sampson, editors, Communicating Process Architectures 2012. Pages 135–154. August, 2012. |
|
[2] |
On the expressiveness of CSP A.W. Roscoe 2011. Draft of February 2011‚ which is very different from previous draft (2008). |
|
[3] |
Specification of communicating processes: temporal logic versus refusals−based refinement Gavin Lowe In Formal Aspects of Computing. 2008. |
|
[4] |
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. |
|
[5] |
The three Platonic models of divergence−strict CSP A.W. Roscoe In Proceedings of ICTAC '08. 2008. |
|
[6] |
Revivals‚stuckness and the hierarchy of CSP Models A. W. Roscoe December, 2008. to appear (revision of 2005 and 2007 drafts) |
|
[7] |
Formal verification of not fully symmetric systems using counter abstraction Tomasz Mazur In Proceedings of the MOdelling and VErifying Process (MOVEP'08). 2008. |
|
[8] |
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. |
|
[9] |
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. |
|
[10] |
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 |
|
[11] |
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. |
|
[12] |
Nets with Tokens Which Carry Data A. W. Roscoe‚ Ranko Lazic‚ Tom Newcomb‚ Joel Ouaknine and James Worrell In Springer LNCS 3349. 2007. Details | BibTeX | Download | Download (pdf) |
|
[13] |
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. |
|
[14] |
On CSP refinement tests that run multiple copies of a process Gavin Lowe 2007. |
|
[15] |
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. |
|
[16] |
On Timed Models and Full Abstraction Gavin Lowe and Joël Ouaknine In Electr. Notes Theor. Comput. Sci.. Vol. 155. Pages 497−519. 2006. |
|
[17] |
Modelling unbounded parallel sessions of security protocols in CSP A. W. Roscoe and E. Kleiner 2006. |
|
[18] |
Verifying Statemate Statecharts Using CSP and FDR A. W. Roscoe and 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 |
|
[19] |
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. |
|
[20] |
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. |
|
[21] |
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 |
|
[22] |
Machine−Verifiable Responsiveness A. W. Roscoe‚ J. N Reed and J. E Sinclair In Proceedings of AVOCS 2005. 2005. |
|
[23] |
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. |
|
[24] |
Seeing beyond divergence A. W. Roscoe In Communicating Sequential Processes‚ the first 25 years. No. 3525. Springer LNCS. 2005. |
|
[25] |
The pursuit of buffer tolerance A. W. Roscoe May, 2005. unpublished draft |
|
[26] |
A Hierarchy of Failures−Based Models Christie Bolton and Gavin Lowe In Electr. Notes Theor. Comput. Sci.. Vol. 96. Pages 129−152. 2004. |
|
[27] |
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. |
|
[28] |
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. |
|
[29] |
Finitary refinement checks for infinitary specifications A. W. Roscoe In Proceedings of CPA 2004. June, 2004. |
|
[30] |
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. |
|
[31] |
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. |
|
[32] |
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. |
|
[33] |
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. |
|
[34] |
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. |
|
[35] |
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 |
|
[36] |
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. |
|
[37] |
Compiling Statemate Statecharts into CSP and verifying them using FDR A. W. Roscoe January, 2003. Extended Abstract |
|
[38] |
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 | BibTeX | Download (ps.gz) | Link |
|
[39] |
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 |
|
[40] |
Capturing parallel attacks within the data independence framework A. W. Roscoe and P. J. Broadfoot In Proceedings of CSFW 15. IEEE Press. 2002. |
|
[41] |
Internalising Agents in CSP Protocol Models A. W. Roscoe and P. J. Broadfoot In Proceedings of WITS 2002. 2002. Extended Abstract |
|
[42] |
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. |
|
[43] |
What can you Decide about Resetable Arrays? A. W. Roscoe and R. S. Lazic In Proceedings of VCL 2001. 2001. |
|
[44] |
Compiling Shared Variable Programs into CSP A. W. Roscoe In Proceedings of PROGRESS workshop 2001. 2001. |
|
[45] |
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. |
|
[46] |
Automating Data Independence A. W. Roscoe‚ P.J. Broadfoot and G. Lowe In Proceedings of ESORICS2000. Vol. 1895. LNCS. 2000. |
|
[47] |
Data independent induction over structured networks A. W. Roscoe and S.J. Creese In Proceedings of PDPTA2000. 2000. |
|
[48] |
The successes and failures of behavioural models A. W. Roscoe‚ R. Forster and G.M. Reed In Millennial Perspectives in Computer Science. Palgrave. 2000. |
|
[49] |
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. |
|
[50] |
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. |
|
[51] |
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. |
|
[52] |
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. |
|
[53] |
Proving security protocols with model checkers by data independence techniques A. W. Roscoe In Proceedings of CSFW 1998. IEEE Press. 1998. |
|
[54] |
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/ |
|
[55] |
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. |
|
[56] |
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. |
|
[57] |
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) |
|
[58] |
Probabilistic and Prioritized Models of Timed CSP Gavin Lowe In Theor. Comput. Sci.. Vol. 138. No. 2. Pages 315−352. 1995. Details | BibTeX | DOI (10.1016/0304-3975(94)00171-E) | Link |
|
[59] |
Scheduling−Oriented Models for Real−Time Systems Gavin Lowe In The Computer Journal. Vol. 38. No. 6. Pages 443−456. 1995. |
|
[60] |
Refinement of Complex Systems: A Case Study Gavin Lowe and Hussein Zedan In The Computer Journal. Vol. 38. No. 10. Pages 785−800. 1995. |
|
[61] |
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 |
|
[62] |
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. |
|
[63] |
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. |
|
[64] |
A Classical Mind: essays in Honour of C.A.R. Hoare A. W. Roscoe, editor Prentice−Hall. 1994. |
|
[65] |
Model−checking CSP A. W. Roscoe In A Classical Mind: essays in Honour of C.A.R. Hoare. Chapter 21. Prentice−Hall. 1994. |
|
[66] |
Probabilities and Priorities in Timed CSP Gavin Lowe PhD Thesis , type=DPhil thesis DPhil thesisType. Oxford University Computing Laboratory. 1993. |
|
[67] |
Denotational semantics for occam II A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott No. PRG−108. Oxford University Computing Laboratory. 1993. |
|
[68] |
Developing and verifying protocols in CSP A. W. Roscoe In Proceedings of Mierlo workshop on protocols. TU Eindhoven. 1993. |
|
[69] |
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 |
|
[70] |
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. |
|
[71] |
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. |
|
[72] |
A semantic model for occam II A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott In Proceedings of Transputing. Vol. 93. 1991. |
|
[73] |
Deadlock analysis in networks of communicating processes A. W. Roscoe and S.D. Brookes In Distributed Computing. No. 4. Pages 209–230. 1991. |
|
[74] |
CSP and timewise refinement A. W. Roscoe‚ G. M. Reed and S. A. Schneider In Proceedings of the BCS−FACS Refinement Workshop. LNCS. 1991. |
|
[75] |
Maintaining consistency in distributed databases A. W. Roscoe No. PRG−87. Oxford University Computing Laboratory. 1990. |
|
[76] |
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. |
|
[77] |
A temporal logic for Timed CSP D.M. Jackson‚ J.W. Davies‚ G.M. Reed and S.A. Schneider Esprit SPEC project. 1990. |
|
[78] |
Unbounded nondeterminism in CSP A. W. Roscoe and G.Barrett In Proceedings of MFPS89. No. 298. Springer. 1989. |
|
[79] |
A timed model for communicating sequential processes A. W. Roscoe and G.M. Reed In Theoretical Computer Science. Vol. 58. Pages 249–261. 1988. |
|
[80] |
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. |
|
[81] |
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) |
|
[82] |
Transforming occam programs A. W. Roscoe and M.H. Goldsmith In The Design and Application of Parallel Digital Processors. No. 298. 1988. |
|
[83] |
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. |
|
[84] |
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 |
|
[85] |
The pursuit of deadlock freedom A. W. Roscoe and Naiem Dathi In Information and Computation. Vol. 75. No. 3. Pages 289–327. December, 1987. |
|
[86] |
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.. |
|
[87] |
An Operational Semantics for CSP A. W. Roscoe‚ S. D. Brookes and D. J. Walker Oxford University Computing Laboratory. 1986. |
|
[88] |
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. |
|
[89] |
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. |
|
[90] |
Proceedings of the Pittsburgh seminar on concurrency A. W. Roscoe‚ S.D. Brookes and G. Winskel, editors A. W. Roscoe‚ S.D. Brookes and G. Winskel, editors |
|
[91] |
Denotational semantics for occam A. W. Roscoe In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 306–329. Springer. 1985. |
|
[92] |
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. |
|
[93] |
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. |
|
[94] |
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. |
|
[95] |
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. |
|
[96] |
Programs as executable predicates A. W. Roscoe and C.A.R. Hoare In Proceedings of FGCS84 (ICOT‚ editors). Pages 220–228. 1984. |
|
[97] |
A mathematical theory of communicating processes A. W. Roscoe PhD Thesis , type=D. Phil. thesis D. Phil. thesisType. Oxford University. 1982. Please note this is a 270 page‚ 118 Mb scanned file and will take some time to download. |
|
[98] |
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. |