Kurssin alustava ohjelma
Wed 17.1
- Ch. 1: Introduction, p. 1-11, Keijo Heljanko
Wed 24.1
- Ch. 2: Modeling Systems, p. 13-26, Emil Falck
- Ch. 3: Temporal Logics, p. 27-33, Niko Cankar
Wed 31.1
- Ch. 4.2: LTL Model Checking by Tableau, p. 41-46, G. Varro
Wed 7.2
- Ch. 4.3: CTL* Model Checking, p. 46-49, Niko Cankar
- Ch. 5: Binary Decision Diagram, p. 51-59, Emil Falck
Wed 14.2
- Ch. 6-6.1: Symbolic Model Checking: Fixpoints, P. 61-66, G. Varro
- Ch. 4-4.1: Model Checking CTL, p. 35-41, Niko Cancar
Wed 21.2
- Ch. 6.4-6.5: Counterexamples, An Alu Example, p. 71-77, Emil Falck
- Ch. 6.6: Relational Product Computations, p. 77-87, G. Varro
Wed 28.2
- Home exercise distribution, Keijo Heljanko
- Ch. 6.7: Symbolic LTL Model Checking, p. 87-95, Timo Latvala
Wed 7.3
- Ch. 7: Mu-Calculus, p. 97-108, Keijo Heljanko
- Ch. 9-9.3: Model Checking and Automata Theory, p. 121-132, Niko Cankar
Wed 14.3 (not G. Varro)
- Ch. 6.2-6.3: Symbolic Model Checking for CTL, Fairness, p. 66-71, Emil Falck
- Ch. 8: Model Checking in Practice, p. 109-120, Niko Cancar
Wed 21.3
- Ch. 9.4-9.6, Translating LTL into Automata, p. 132-140, Emil Falck
- Ch. 10-10.4, Partial Order reductions, p. 141-154, G. Varro
Wed 28.3
- Home exercise deadline
- Ch. 10.5-10.7: Ample Sets + Spin, p. 154-170, Keijo Heljanko
- Ch. 11: Equivalences + Preorders, p. 171-184, Timo Latvala
Wed 4.4
- G. Holzmann and M. H. Smith: Software Model Checking, Niko Cankar
- A. Biere, A. Cimatti, E. Clarke, and Y. Zhu: Symbolic model checking
without BDDs, G. Varro
Wed 11.4
- P.A. Abdulla, P. Bjesse, and N. Eén: Symbolic reachability analysis using
SAT solvers, Emil Falck
- P. Wolper, U. Stern, D. Leroy and D. L. Dill: Reliable Probabilistic Verification
Using Hash Compaction, Keijo Heljanko
Wed 18.4
- Easter vacation, no seminar!
Wed 25.4
- J. Esparza and S. Schwoon: A BDD-based Model Checker for Recursive Programs, G. Varro
- Guest lecture: N.N.