Preliminary course schedule
Wed 16.1
- Introduction, Heljanko
- Systems and Software Verification: Automata, Chapter 1-1.5, pages 5-18, Keinänen
Wed 23.1
- Systems and Software Verification: Synchronization, Chapter 1.5-1.7, pages 19-26, Dubrovin
- Systems and Software Verification: Temporal logics, Chapter 2-2.2, pages 27-33, Kettula
Wed 30.1
- Systems and Software Verification: Temporal logics, Chapter 2.3-2.4, pages 33-38, Slavov,
- Systems and Software Verification: Reachability + Deadlock freeness, Intro + Chapter 6 + Chapter9, pages 77-81, 99-101, Keinänen
Wed 6.2
- Systems and Software Verification: Safety, Chapter 7, pages 83-89, Honkola
- Systems and Software Verification: Liveness, Chapter 8, pages 91-98, Kettula
- Systems and Software Verification: Fairness, Chapter 10, pages 103-107, Dubrovin
Wed 13.2
- Homework distribution.
- Systems and Software Verification: Safety, Chapter 7 (continuation), Honkola
- Systems and Software Verification: Abstraction, Chapter 11, pages 109-125, Heljanko
- Model Checking: Buchi automata, Chapter 9-9.2, pages 121-127, Slavov
Wed 20.2
- Systems and Software Verification: Abstraction, Chapter 11 (continuation), Heljanko
- Model Checking: Emptiness checking, Chapter 9.2.1-9.3, pages 127-132, Honkola
- Model Checking: LTL to Buchi automata, Chapter 9.4-9.5, pages 132-139, Keinänen
Wed 27.2
- Model Checking: Partial Order Reduction, Chapter 10-10.2, pages 141-147, Kettula
- Model Checking: Partial Orders for LTL-X, Chapter 10.3-10.4, pages 147-154, Dubrovin
Wed 6.3
- Model Checking: LTL to Buchi automata, Chapter 9.4-9.5 (continuation), Keinänen
- Model Checking: Complexity + Heuristics, Chapter 10.5.1-10.5.2, pages 154-159, Keinänen
- Model Checking: On-the-fly + Correctness, Chapter 10.5.3-10.6, pages 159-164, Honkola
Wed 13.3
- Homework deadline
- Model Checking: PO in SPIN, Chapter 10.7, pages 164-170, Kettula
- On-the-fly testing, Heljanko
Wed 20.3
- P. Wolper, U. Stern, D. Leroy and D. L. Dill: Reliable Probabilistic Verification Using Hash Compaction, Dubrovin
Wed 27.3
Wed 3.4
- Easter holiday, no seminar!
Thu 4.4 11.15-12.45 TB353
- W. Visser, K. Havelund, G. Brat and S. Park: Model Checking Programs, Slavov
Wed 10.4
Wed 17.4
- S. Chandra, P. Godefroid, and C. Palm: Software Model Checking in Practice: An Industrial Case Study, Dubrovin
- J. Hatcliff, J. Corbett, M. Dwyer, S. Sokolowski, and H. Zheng: A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, Honkola
- A. Biere, E. M. Clarke, R. Raimi, and Y. Zhu: Verifying Safety Properties of a PowerPC[tm] Microprocessor Using Symbolic Model Checking without BDDs, Keinänen
Fri 19.4 11.15-12.45 TB353
- Homework feedback, Heljanko
- U. Stern and D. L. Dill: Parallelizing the Murphi Verifier, Slavov
- G. J. Holzmann and M. H. Smith: Software Model Checking - Extracting Verification Models from Source Code, Kettula
Wed 24.4
- T. Ball, S. K. Rajamani: Automatically Validating Temporal Safety Properties of Interfaces, Honkola
- J. Esparza, D. Hansel, P. Rossmanith, and S. Scwoon: Efficient Algorithms for Model Checking Pushdown Systems, Slavov
- T. Junttila: Symmetries in Model Checking