Preliminary course schedule
Mon 24.1
- Lecture: Introduction and Automata on Finite Words
- Lecture: Automata on Finite Words, part II
Mon 31.1
- Distribution of 1st home exercise
- Lecture: Kripke structures, part I
- Lecture: Temporal logic LTL, part I
Mon 7.2
- Lecture: Temporal logic LTL, part II
- Systems and Software Verification: Automata, Chapter 1.1-1.5, pages 1-18, Yrjölä
- U. Stern, D. L. Dill: Parallelizing the Murphi verifier, Rusanen
Mon 14.2
- Distribution of 2nd home exercise
- Lecture: Temporal logic LTL, part III
- Systems and Software Verification: Synchronization, Chapter 1.5-1.7, pages 19-26, Pohjolainen
Mon 21.2 16:15-17:00
- Deadline of 1st home exercise
- Tutorial: Answers to the 1st home exercise
Mon 28.2
- Deadline of 2nd home exercise
- Distribution of 3rd home exercise
- Lecture: Automata on Infinite Words, part I
- P. Wolper, U. Stern, D. Leroy and D. L. Dill: Reliable Probabilistic Verification Using Hash Compaction, Terhivuo
- Tutorial: Answers to the 2nd home exercise
Mon 7.3
- Lecture: Automata on Infinite Words, part II
- Systems and Software Verification: Temporal logics, Chapter 2-2.2, pages 27-33, Yrjölä
- Systems and Software Verification: Temporal logics, Chapter 2.3-2.4, pages 33-37, Pohjolainen
Thu 10.3 9:15-12:00 B353
- Lecture: Büchi Automata Algorithms, Translating LTL to Büchi Automata, part I
- Lecture: Translating LTL to Büchi Automata, part II
- Systems and Software Verification: Reachability + Deadlock freeness, Intro + Chapter 6 + Chapter 9, pages 77-81, 99-101, Rusanen
Mon 14.3
- Deadline of 3rd home exercise
- Distribution of 4th home exercise
- Lecture: Translating LTL to Büchi Automata, part III
- Systems and Software Verification: Safety, Chapter 7, pages 83-89, Linnanto
- Tutorial: Answers to the 3rd home exercise
Mon 21.3
- Lecture: Model Checking under Fairness
- Systems and Software Verification: Liveness, Chapter 8, pages 91-98, Terhivuo
- Systems and Software Verification: Fairness, Chapter 10, pages 103-107, Yrjölä
Mon 28.3
- Easter vacation, no lectures or tutorials!
Mon 4.4
- Deadline of 4th home exercise
- Distribution of 5th home exercise
- Systems and Software Verification: Abstraction, Chapter 11, pages 109-125, Linnanto
- Model Checking: Partial Order Reduction, Chapter 10-10.2, pages 141-147, Rusanen
- Tutorial: Answers to the 4th home exercise
Mon 11.4
- Description of a Master's Thesis project, Pohjolainen
- Model Checking: Partial Orders for LTL-X, Chapter 10.3-10.4, pages 147-154, Terhivuo
- Model Checking: Complexity + Heuristics, Chapter 10.5.1-10.5.2, pages 154-159, Yrjölä
Mon 18.4
- Deadline of 5th home exercise
- Model Checking: On-the-fly + Correctness, Chapter 10.5.3-10.6, pages 159-164, Linnanto
- T. Ball et. al: SLAM and Static Driver Verifier, Terhivuo
- Tutorial: Answers to the 5th home exercise
Mon 25.4
- Lecture: On-the-fly Model Checking, Abstraction
- G. J. Holzmann: The Model Checker Spin, Pohjolainen
- Model Checking: PO in SPIN, Chapter 10.7, pages 164-170, Rusanen
Mon 2.5
- W. Visser, K. Havelund, G. Brat and S. Park: Model Checking Programs, Linnanto
- Guest lecture: N.N.