Kurssin alustava ohjelma
ke 20.1
- Godefroid Ch. 1-2 pp. 11-26, (Intro, LFCS model), Heljanko
ke 27.1
- Godefroid Ch. 3-3.3, pp. 27-32, (Traces), Latvala
- U. Stern and D. L. Dill: Parallelizing the Murphi Verifier, Tarkkala
- Valmari Ch. 1-2.2, pp. 429-439, (Concepts, Abstractions), Syrjänen
ke 3.2
- Godefroid Ch. 3.4, pp. 33-40, (Independency), Heljanko
- Valmari Ch. 2.3-2.4, pp. 439-444, (Linear/Branching Time, Safety,
Liveness, Fairness), Lehtonen
- G. J. Holzmann: State Compression in SPIN: Recursive Indexing and
Compression Training Runs, Tauriainen
ke 10.2
- Godefroid Ch. 4-4.4, pp. 41-50, (Persistent Sets: Alg1, Alg2:Overman),
Tarkkala
- Valmari Ch. 3-4.2 (on-the-fly not included), pp. 444-451,
(Structure, Terms, Statistics), Latvala
ke 17.2
- U. Stern, D. L. Dill: A New Scheme for Memory-Efficient Probabilistic
Verification, Heljanko
ke 24.2
- Godefroid Ch. 4.5-4.6, pp. 51-60, (Strong Stubborn Sets), Lehtonen
- Godefroid Ch. 4.7-4.8, pp. 60-70, (Weak Stubborn Sets), Tauriainen
- Valmari Ch. 4.2 (on-the-fly), pp. 451-455, (On-the-fly), Syrjänen
ke 3.3 - Harjoitustöiden jako -
- Valmari Ch. 4.3, pp. 455-460, (Temporal logics), Latvala
- Valmari Ch. 5, pp. 473-478, (Complexity), Syrjänen
- C. Coucerbetis, M. Vardi, P. Wolper, and M. Yannakakis: Memory-Efficient
Algorithms for the Verification of Temporal Properties, Tarkkala
ke 10.3
- Godefroid Ch. 5, pp. 71-80, (Sleep Sets), Heljanko
- Godefroid Ch. 6, pp. 81-98, (Safety Property Verification), Tarkkala
- Valmari Ch. 6-7.1, pp. 478-486, (Reduction Strategies,
Preprocessing), Lehtonen
ke 17.3
- Godefroid Ch. 7, pp. 99-108, (Liveness), Syrjänen
- Valmari Ch. 7.2, pp. 486-492, (Packed State Spaces, Supertrace,
Coverability, Symmetry), Tauriainen
- H. R. Andersen: An Introduction to Binary Decision Diagrams,
Latvala
ke 22.3 - Ei seminaaria, luennoitsija matkoilla -
ke 31.3
- Godefroid Ch. 8-8.3, pp. 109-116, (Results), Lehtonen
- Valmari Ch. 7.2, pp. 493-497, (Unfolding, OBDD), Latvala
ke 7.4 - Ei seminaaria, pääsiäisloma -
ke 14.4 - Harjoitustöiden palautus
- Godefroid Ch. 8.4-9.2, pp. 116-126, (Caching, Conclusions), Syrjänen
- Valmari Ch. 7.4 (static definitions not included), pp. 501-505
(Stubborn Sets Basics), Tarkkala
- R. Gerth, D. Peled, M. Y. Vardi and P. Wolper: Simple
On-the-fly Automatic Verification of Linear Temporal
Logic, Tauriainen
ke 21.4
- Valmari Ch. 7.4 (static definitions included)-7.4 (safety
properties not included), pp. 505-509, (Static Stubborn Sets), Latvala
- Valmari 7.4 (safety properties), pp. 509-512, (Stubborn Sets for
Safety), Lehtonen
ke 28.4
- Valmari 7.4 (liveness properties), pp. 512-517, (Stubborn Sets
for Liveness), Tauriainen
- Valmari 7.4 (branching time properties + sleep sets),
pp. 517-520, (Stubborn Sets for Branching Properties), Tarkkala
- Verification Based on the Finite Complete Prefix, Heljanko
ke 5.5
- Valmari 8, pp. 521-523, (Conclusions), Syrjänen
- Symmetries, Junttila
- Harjoitustyöpalaute + Yhteenveto, Heljanko