Preliminary course schedule
Tue 17.1
- Lecture: Introduction, course requirements
Tue 31.1 Modeling reactive systems with automata
- Distribution of Home Exercise 1
- Systems and Software Verification: Automata, Chapter 1.1-1.4, pages 5-14, Lehmann
- Systems and Software Verification: Synchronization, Chapter 1.5-1.7, pages 14-26, Lönnberg
Tue 7.2 Temporal logics
- Systems and Software Verification: Temporal logics, Chapter 2-2.4, pages 27-37, Ojala
Tue 14.2 Specifying with temporal logics
- Systems and Software Verification: Reachability+Deadlock-freeness,
Intro+Chapter 6 + Chapter 9, pages 77-81 and 99-101, Reya
Tue 21.2 Specifying with temporal logics
- Deadline for Home Exercise 1, Distribution of Home Exercise 2
- Systems and Software Verification: Safety, Chapter 7, pages 83-89, Lehmann
- Systems and Software Verification: Liveness + Fairness, Chapter 8 + Chapter 10, pages 91-98 and 103-107, Lönnberg
Tue 28.2 Model checking
- Distribution of Project Work
- Model Checking: CTL Model Checking, Chapter 4.1, pages 35-41, Ojala
Tue 7.3 No lecture
Tue 14.3 No lecture
Tue 21.3 Alleviating state space explosion problem
- Deadline for Home Exercise 2, Distribution of Home Exercise 3
- Model Checking: Partial Order Reduction, Chapter 10-10.2, pages 141-147, Reya
- Model Checking: Partial Orders for LTL-X, Chapter 10.3-10.4, pages 147-154, Lönnberg
Tue 28.3 Model checking, alleviating state space explosion problem
- Model Checking: LTL Model Checking Using Automata, Chapter 9.1-9.3, pages 121-132, Lehmann
- Model Checking: Complexity + Heuristics, Chapter 10.5.1-10.5.2, pages 154-159, Reya
Tue 4.4 Scientific articles
- S. Chandra, P. Godefroid and C. Palm: Software Model Checking in Practice, Reya
Sun 9.4 Deadline for Project Work
Tue 11.4 Alleviating state space explosion problem, scientific articles
- Deadline for Home Exercise 3
- Model Checking: On-the-fly + Correctness, Chapter 10.5.3-10.6, pages 159-164, Ojala
- J. Geldenhuys and A. Valmari: More Efficient On-the-fly LTL Verification with Tarjan's Algorithm, Lehmann
- W. Visser, K. Havelund, G. Brat and S. Park: Model Checking Programs, Lönnberg
- G. J. Holzmann: The Model Checker Spin, Ojala