Vaihtuvasisältöinen lisensiaattikurssi. Syksyn 2001 aiheena on mallintarkastus (model-checking).

Mallintarkastus on nousemassa yhdeksi tietokoneavusteisen suunnittelun keskeiseksi työkaluksi, jolla voidaan varmentaa tehtyjen suunnitelmien ja toteutusten oikeellisuutta ja laatua. Mallintarkastus on otettu jo laajamittaisesti käyttöön digitaalipiirien suunnittelussa ja sen hyödyntäminen myös ohjelmistosuunnittelussa on siirtymässä tutkimuksesta käytäntöön. Seminaarissa tutustutaan mallintarkastukseen perusteista lähtien käymällä läpi sen pohjalla olevaa teoriaa (automaattiteoria ja temporaalilogiikka), mallintarkastuksen automatisointiin liittyviä kysymyksiä, nykyisin tarjolla olevia työkaluja ja sovellutuksia.

• Vastaava opettaja: Prof. Ilkka Niemelä, TB337, puh. 451 3290, email: Ilkka.Niemela@hut.fi
• Kurssi suoritetaan seminaarimuotoisesti pitämällä seminaariesitelmiä ja tekemällä kotitehtäviä.
• Seminaaritilaisuudet: maanantaisin klo 16.30-19.30, TB353 (TT-talo)
• Ensimmäinen kokoontuminen ma 10.9.2001 klo 16.30 (järjestäytymistilaisuus)
• Materiaali:
  • B. Berard et al., Systems and Software Verification, Model-Checking Techniques and Tools. Springer, 2001.
  • E.M. Clarke and B. Schlingloff, Model Checking. Handbook of Automated Reasoning edited by A. Robinson and A. Voronkov. Elsevier, 2001.
  • P. Bjesse, Gate Level Description of Synchronous Hardware and Automatic Verification Based on Theorem Proving. Doctoral Dissertation, Department of Computing Science, Chalmers University of Technology, 2001. [ps.gz]
• Kurssin suorittaminen
• Kurssin ohjelma, tutkielmat, sekä kotitehtävät
• Lisätehtävät 21.12.2001 ([PS] [PDF]). Viimeinen palautuspäivä 15.1.2002; arvostelu 0-1.5 p/tehtävä.
• Kotitehtäväpisteet
• Kevään 2001 kurssi