Preliminary course schedule
Wed 14.1
- Lecture: Introduction
- Lecture: Automata on Finite Words, part I
- Distribution of 1st home exercise
Wed 21.1
- Lecture: Automata on Finite Words, part II
- Systems and Software Verification: Automata, Chapter 1.1-1.4, pages 1-14, Lindqvist
- Systems and Software Verification: Synchronization, Chapter 1.5-1.7, pages 14-26, Hirsimäki
Wed 28.1
- Lecture: Kripke Structures and Automata
- U. Stern, D. L. Dill: Parallelizing the Murphi verifier, Oikarinen
- Systems and Software Verification: Temporal logics, Chapter 2-2.2, Lindqvist
Wed 4.2
- Deadline of 1st home exercise
- Tutorial: Answers to the 1st home exercise
- Distribution of 2nd home exercise
- Lecture: Temporal logic LTL, CTL, and CTL*, part I
- Systems and Software Verification: Temporal logics, Chapter 2.3-2.4, Karilinna
Wed 11.2
- Lecture: Temporal logic LTL, CTL, and CTL*, part II
- S. Chandra, P. Godefroid, and C. Palm: Software Model Checking in Practice: An
Industrial Case Study, Ruusu
- Systems and Software Verification: Reachability + Deadlock freeness,
Intro + Chapter 6 + Chapter 9, pages 77-81, 99-101, Chou
Wed 18.2
- Deadline of 2nd home exercise
- Distribution of 3rd home exercise
- Tutorial: Answers to the 2nd home exercise
- J. Geldenhuys and A. Valmari: A Nearly Memory-optimal Data Structures for Sets and Mappings, Martinez
Wed 25.2
- Lecture: Büchi Automata, part I
- Lecture: Büchi Automata, part II
Wed 3.3
- Deadline of 3rd home exercise
- Distribution of 4th home exercise
- Tutorial: Answers to the 3rd home exercise
- Systems and Software Verification: Safety, Chapter 7, pages 83-89, Martinez
- G. J. Holzmann and Anuj Puri: A Minimized Automaton Representation of States, Chou
Wed 10.3
- Systems and Software Verification: Liveness, Chapter 8, pages 91-98, Karilinna
- P. Wolper, U. Stern, D. Leroy and D. L. Dill: Reliable Probabilistic Verification Using Hash Compaction, Hirsimäki
- Systems and Software Verification: Fairness, Chapter 10, pages 103-107, Ruusu
Wed 17.3
- Deadline of 4th home exercise
- Tutorial: Answers to the 4th home exercise
- Distribution of 5th home exercise
- Lecture: Büchi Automata Algorithms, Translating LTL to Büchi Automata, part I
- W. Visser, K. Havelund, G. Brat and S. Park: Model Checking Programs, Karilinna
Wed 24.3
- Lecture: Translating LTL to Büchi Automata, part II
- Model Checking: Partial Order Reduction, Chapter 10-10.2, pages 141-147, Ruusu
- Systems and Software Verification: Abstraction, Chapter 11, pages 109-125, Martinez
Wed 31.3
- Deadline of 5th home exercise
- Tutorial: Answers to the 5th home exercise
- Model Checking: Partial Orders for LTL-X, Chapter 10.3-10.4, pages 147-154, Chou
Wed 7.4
- Lecture: Translating LTL to Büchi Automata, part III
- Lecture: Model Checking under Fairness
- Model Checking: Equivalences and Preorders, Chapter 11, pages 171-178, Hirsimäki
Wed 14.4 - Easter vacation. No lectures or tutorials.
Wed 21.4
- Distribution of the bonus exercise.
- Model Checking: Complexity + Heuristics + On-the-fly, Chapter 10.5.1-10.5.3,
pages 154-160, Lindqvist
- I. Beer: Efficient Detection of Vacuity in Temporal Model Checking.
- (double), Emilia
Wed 28.4
- Deadline of the bonus exercise.
- Lecture: Model Checking tools
- Invited talk: Kimmo Varpaaniemi: On Partial Order Reductions