- 担当教員：小林直樹
- 講義日：火曜２限（10:25-12:10）
- 講義室：理学部7号館214号室
- 休講: 9/24
- Contact：
- Subjects： This year, we plan to cover process calculi (such as CCS and pi-calculus) and their applications to verification of concurrent systems/programs and security protocols.
- References:
- R. Milner, Communication and Concurrency, Prentice Hall, 1989
- R. Milner, Communicating and Mobile Systems: the p-calculus, Cambridge University Press, 1999
- D. Sangiorgi and D. Walker, The p-calculus: A Theory of Mobile Processes, Cambridge University Press, 2001
- C. Stirling, Modal and Temporal Properties of Processes, Springer, 2001

- slides and lecture notes (protected by a password, which will be announced in the first lecture)
- CCS: syntax and operational semantics
- CCS: process equivalence 1 (trace equivalence and strong bisimilulation)
- CCS: process equivalence 2 (weak bisimulation and simulation; co-induction)
- CCS: process equivalence 3 (tools and techniques for proving bisimulation; testing equivalence)
Sample inputs for CAAL (Concurrency Workbench, Aalborg Version)

- CCS: modal logics for processes
Sample inputs for verification of Peterson's algorithm

- pi-calculus: syntax and operational semantics
- pi-calculus: process equivalence
- pi-calculus: type systems and typed process equivalence The tool TyPiCal, demonstrated in the lecture, is available here.
- spi-calculus and verification of security protocols

- About homework:
Homework assignments will be announced through ITC-LMS, and reports on them should also be submitted through ITC-LMS. Plagiarism is strictly prohibited. See also this page.

Previous homeworks and partial solutions for them are available here.