Kurssin alustava ohjelma
ke 26.1
- U. Stern, D. L. Dill: A New Scheme for Memory-Efficient Probabilistic
Verification, Heljanko
ke 2.2
- Valmari Ch. 1-2.2, pp. 429-439, (Concepts, Abstractions), Kilponen
- U. Stern and D. L. Dill: Parallelizing the Murphi Verifier, Anderson
ke 9.2
- Kotitehtävien jako, Heljanko
- Valmari Ch. 2.3-2.4, pp. 439-444, (Linear/Branching Time, Safety,
Liveness, Fairness), Heljanko
ke 16.2
- Valmari Ch. 3-4.2 (on-the-fly not included), pp. 444-451,
(Structure, Terms, Statistics), Anderson
ke 23.2
- Courcoubetis et.al. : Memory-Effient Algorithms for the Verification of
Temporal Properties, Tynjälä
- G. J. Holzmann et.al. : A Minimized Automaton Representation of
Reachable States, Kilponen
ke 1.3
- Valmari Ch. 4.2 (on-the-fly), pp. 451-455, (On-the-fly), Tynjälä
ke 8.3
- Valmari Ch. 4.3, pp. 455-460, (Temporal logics), Heljanko
- Valmari Ch. 5, pp. 473-478, (Complexity), Anderson
ke 15.3
- Valmari Ch. 6-7.1, pp. 478-486, (Reduction Strategies,
Preprocessing), Kilponen
ke 22.3
- Valmari Ch. 7.2, pp. 486-492, (Packed State Spaces, Supertrace,
Coverability, Symmetry), Tynjälä
ke 29.3
- Valmari Ch. 7.4 (static definitions not included), pp. 501-505
(Stubborn Sets Basics), Kilponen
ke 5.4 Kotitehtävien palautus
- Valmari Ch. 7.2, pp. 493-497, (Unfolding, OBDD), Heljanko
ke 12.4
- Valmari Ch. 7.4 (static definitions included)-7.4 (safety
properties not included), pp. 505-509, (Static Stubborn Sets), Tynjälä
- Gerth et.al.: Simple On-the-fly Automatic Verification of LTL, Anderson
ke 19.4
- Valmari 7.4 (safety properties), pp. 509-512, (Stubborn Sets for
Safety), Tynjälä
- Valmari 7.4 (liveness properties), pp. 512-517, (Stubborn Sets
for Liveness), Kilponen
ke 26.4 Ei seminaaria - pääsiäisloma
ke 3.5
- Valmari 7.4-8 (branching time properties + sleep sets),
pp. 517-523, (Stubborn Sets for Branching Properties + Conclusions), Anderson
- Guest lecture, N.N.