Concurrency: 20172018
Lecturer 

Practical Coordinator 

Degrees 
Schedule S1(CS&P) — Computer Science and Philosophy Schedule B1 (CS&P) — Computer Science and Philosophy Schedule S1 — Computer Science Schedule B1 — Computer Science Schedule S1(M&CS) — Mathematics and Computer Science Schedule B1 — Mathematics and Computer Science 
Term 
Trinity Term 2018 (16 lectures) 
Links
FDR: the CSP refinement checker
Overview
Learning outcomes
At the end of the course the student should:
 understand some of the issues and difficulties involved in Concurrency;
 be able to specify and model concuurent systems using CSP;
 be able to reason about CSP models of systems using both algebraic laws and semantic models;
 be able to analyse CSP models of systems using the model checker FDR.
Synopsis
 Processes and observations of processes; point synchronisation, events, alphabets. Sequential processes: prefixing, choice, nondeterminism. Operational semantics; traces; algebraic laws. [3]
 Recursion. Complete partial orders and fixed points as a means of explaining recursion; approximation, limits, least fixed points; guardedness and unique fixed points. [1]
 Concurrency. Hiding. Renaming. [3]
 Nondeterministic behaviours, refusals, failures; the determinism ordering. [2]
 Hiding and divergence, the failuresdivergences model. [1]
 Specification and correctness. [2]
 Communication, pipes, buffers. Sequential composition. [2]
 Case study. [2]
Syllabus
Reading list
Lecture Notes: The lecture notes for this year's course will be given out in lectures as the course progresses. They will only appear online on the Course Materials page with a significant delay.
Course Text:
 A. W. Roscoe, Understanding Concurrent Systems, Chapters 18, Springer 2010
Alternatives:
 A.W. Roscoe, The Theory and Practice of Concurrency, Chapters 17, PrenticeHall International, 1997; http://www.cs.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf.
 C. A. R. Hoare, Communicating Sequential Processes, PrenticeHall International, 1985; http://www.usingcsp.com.
 S. A. Schneider, Concurrent and Realtime Systems, Chapters 18, Wiley, 2000; http://www.computing.surrey.ac.uk/personal/st/S.Schneider/books/CRTS.pdf.
Overheads: This year's slides will appear on the Course Materials page over the course of the term.
Related research at the Department of Computer Science
Activities 