Digitaalisten järjestelmien lisensiaattikurssi
Syksy 2001

Ohjelma

10.9.:

Järjestäytymistilaisuus

17.9.:

Ei seminaaritilaisuutta

24.9.:

Berard 3-26, Latvala
Berard 27-46, Virtanen
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 8.10.2001)

1.10.:

Berard 47-74, Kaski
Berard 77-98, Luukkala
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 15.10.2001)

8.10.:

Berard 99-123, Leppänen
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 22.10.2001)

15.10.:

Berard 129-177, IN
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 29.10.2001)

22.10.:

Clarke Chapter 1-2, IN (Introduction to model checking, expressiveness)
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 5.11.2001)

29.10.:

Clarke Chapter 3 (Temporal logics and automata), Leppänen (Slides: [PS], [PDF]; Report: [PS], [PDF])
Clarke Chapter 4-5 (Model transformations, properties and reductions), Luukkala (Slides: [PS], [PDF]; Report: [PS], [PDF])
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 12.11.2001)

5.11.:

Clarke Chapter 6-7 (Completeness and decisions procedures), Kaski (Slides: [PS], [PDF]; Report: [PS], [PDF])
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 19.11.2001)

12.11.:

Clarke Chapter 8-9 (Model checking algorithms and modelling of reactive systems), Virtanen (Slides: [PS], [PDF]; Report: [PS], [PDF])

19.11.:

Clarke Chapter 10-12 (Symbolic model checking and partial order techniques), Latvala (Slides: [PS], [PDF]; Report: [PS], [PDF])
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 3.12.2001)

26.11.:

Bjesse Chapter 2 (Lava: Hardware design in Haskell), Luukkala
Bjesse Chapter 3 (Automatic verification of Combinatorial and pipelined FFT circuits), Kaski
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 10.12.2001)

3.12.:

Bjesse Chapter 8, 117-133 (SAT-based model checking), Leppänen
Bjesse Chapter 8, 133-148(SAT-based model checking), Latvala
Bjesse Chapter 7 (Finding Bugs in an Alpha Microprocessor using SAT solvers), Virtanen (Slides: [PS], [PDF])
Kotitehtävät [PS] [PDF] (viimeinen palautuspäivä 27.12.2001)