This is the live page of David Baelde's part of the MPRI 2-30 course, for year 2018-2019.
All sessions take place in room 1003 of the Sophie Germain building.
Lecture notes
I am writing lecture notes as we go; please check out this URL regularly for updated versions.
My lecture notes mostly aim at providing a self-contained account of the semantical aspects of the course, and detailing a few points that are not covered in legacy lecture notes. For some of the course's content, the reference will be these legacy lecture notes, the slides, or an academic article.
Agenda & Teaching Material
- First session: introduction, example modelling and exercise.
- Second session: semantics on the whiteboard, following the lecture notes.
- Third session: deducibility constraints.
- Fourth and fifth sessions: unbounded verification with Proverif, sample files.
- Sixth session: equivalences (we actually started on session five).
- Seventh session: end of equivalences + equivalence verification in Akiss, based on this paper.
- Eight session: a computationally complete symbolic approach for equivalence; see also Comon & Bana, CCS'14 for reference.
Final examination
Try the 2017-18 or 2018-19 exam as an exercise.