Iris Tutorial (original) (raw)
Week
Day
Lecture
Literature
Slides
Hand-in Exercises
1
Day 1
Intro + Operational Semantics
ILN Sec. 1+2
Day 2
Basic Logic of Resources
ILN Sec. 3
ILN Ex. 3.2
2
Day 1
Basic Separation Logic: Hoare Triples
ILN Sec. 4.0
Day 2
Basic Separation Logic: Proving Pointer Programs
ILN Sec. 4.1
ILN Ex. 4.1, 4.2, 4.5, 4.11, 4.21
3
Day 1
Basic Separation Logic: Abstract Data Types
ILN Sec. 4.2
Day 2
Case Study: foldr
ILN Sec. 4.3
ILN Ex. 4.29, 4.34
4
Day 1
Later Modality
ILN Sec. 5
Day 2
Always Modality
ILN Sec. 6
ILN Ex. 5.3, 6.2 item (1) (2) and (4)
5
Day 1
Concurrency: par + invariants
ILN Sec. 7.1 + 7.2
Day 2
Concurrency: ghost state
ILN Sec. 7.4 + 7.5
ILN Ex. 7.6, 7.24 item (3), 7.29, 7.32 (the first triple)
6
Day 1
Concurrency: Case Study: spin lock + concurrent bag
ILN Sec. 7.6
Day 2
Concurrency: Case Study: counter modules
ILN Sec. 7.7
ILN Ex. 7.37, 7.42.
7
Day 1
Weakest preconditions and fancy update modality
ILN Sec. 8.1 + 8.2
Day 2
Concurrency: Case Study: concurrent stack with helping
ILN Sec. 10
ILN Ex. 7.43 (the one for incr), 7.47, 7.49 (the two specs for read).