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.
- Processes and observations of processes; point synchronisation, events, alphabets. Sequential processes: prefixing, choice, nondeterminism. Operational semantics; traces; algebraic laws. 
- Recursion. Complete partial orders and fixed points as a means of explaining recursion; approximation, limits, least fixed points; guardedness and unique fixed points. 
- Concurrency. Hiding. Renaming. 
- Non-deterministic behaviours, refusals, failures; the determinism ordering. 
- Hiding and divergence, the failures-divergences model. 
- Specification and correctness. 
- Communication, pipes, buffers. Sequential composition. 
- Case study. 
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.
- A. W. Roscoe, Understanding Concurrent Systems, Chapters 1-8, Springer 2010
- A.W. Roscoe, The Theory and Practice of Concurrency, Chapters 1-7, Prentice-Hall International, 1997; http://www.cs.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf.
- C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985; http://www.usingcsp.com.
- S. A. Schneider, Concurrent and Real-time Systems, Chapters 1-8, 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