Preliminary course schedule
Wed 15.1
- Lecture: Introduction
- Lecture: Automata on Finite Words, part I
Tue 21.1
- Lecture: Automata on Finite Words, part II
- Distribution of 1st home exercise
Wed 22.1
- Lecture: Kripke structures, part I
- Systems and Software Verification: Automata, Chapter 1.1-1.5, pages 1-18, Rantanen
- Systems and Software Verification: Synchronization, Chapter 1.5-1.7, pages 19-26, Teittinen
Tue 28.1
- Deadline of 1st home exercise
- Distribution of 2nd home exercise
- Lecture: Temporal logic LTL, CTL, and CTL*, part I
- U. Stern, D. L. Dill: Parallelizing the Murphi verifier, Hernando
- Tutorial: Answers to the 1st home exercise
Wed 29.1
- Lecture: Temporal logic LTL, CTL, and CTL*, part II
- Systems and Software Verification: Temporal logics, Chapter 2-2.2, pages 27-33, Gutierrez
- Systems and Software Verification: Temporal logics, Chapter 2.3-2.4, pages 33-37, Teittinen
Tue 4.2
- Deadline of 2nd home exercise
- Distribution of 3rd home exercise
- Lecture: Temporal logic LTL, CTL, and CTL*, part III
- P. Wolper, U. Stern, D. Leroy and D. L. Dill: Reliable Probabilistic Verification Using Hash Compaction, Rantanen
Wed 5.2
- Tutorial: Answers to the 2nd home exercise
- Lecture: Büchi Automata, part I
- Systems and Software Verification: Reachability + Deadlock freeness, Intro + Chapter 6 + Chapter 9, pages 77-81, 99-101, Sancho
- W. Visser, K. Havelund, G. Brat and S. Park: Model Checking Programs, Järvisalo
Tue 11.2
- Deadline of 3rd home exercise
- Distribution of 4th home exercise
- Lecture: Büchi Automata, part II
- Systems and Software Verification: Safety, Chapter 7, pages 83-89, Gutierrez
- Tutorial: Answers to the 3rd home exercise
Wed 12.2
- Systems and Software Verification: Liveness, Chapter 8, pages 91-98, Järvisalo
- Systems and Software Verification: Fairness, Chapter 10, pages 103-107, Rantanen
- G. J. Holzmann: The Model Checker Spin, Teittinen
Tue 18.2
- Deadline of 4th home exercise
- Distribution of 5th home exercise
- Lecture: Büchi Automata Algorithms, Translating LTL to Büchi Automata, part I
- Systems and Software Verification: Abstraction, Chapter 11, pages 109-125, Hernando
- Tutorial: Answers to the 4th home exercise
Wed 19.2
- Lecture: Translating LTL to Büchi Automata, part II
- Model Checking: Partial Order Reduction, Chapter 10-10.2, pages 141-147, Järvisalo
- G. J. Holzmann: An Analysis of Bitstate Hashing, Sancho
Tue 25.2
- Deadline of 5th home exercise
- Lecture: Translating LTL to Büchi Automata, part III
- Model Checking: Partial Orders for LTL-X, Chapter 10.3-10.4, pages 147-154, Gutierrez
- Tutorial: Answers to the 5th home exercise
Wed 26.2
- Lecture: Model Checking under Fairness
- Lecture: Model Checking CTL and CTL*
- Model Checking: Complexity + Heuristics, Chapter 10.5.1-10.5.2, pages 154-159, Sancho
Tue 4.3
- Lecture: On-the-fly Model Checking, Abstraction
- Model Checking: On-the-fly + Correctness, Chapter 10.5.3-10.6, pages 159-164, Hernando
- Model Checking: PO in SPIN, Chapter 10.7, pages 164-170, Heljanko
Wed 5.3
- Lecture: Model Checking tools
- T. Ball, S. K. Rajamani: Automatically Validating Temporal Safety Properties of Interfaces, Latvala
- Invited talk: Tommi Junttila: Symmetries