Vaihtuvasisältöinen lisensiaattikurssi. Kevään 2001 aiheena on symbolinen mallintarkastus.

• Vastaava opettaja: Prof. Ilkka Niemelä, TB337, puh. 451 3290, email: Ilkka.Niemela@hut.fi
• Kurssi suoritetaan seminaarimuotoisesti.
• Seminaaritilaisuudet: maanantaisin klo 16.30-19.30, TB353 (TT-talo)
• Ensimmäinen kokoontuminen ma 15.1.2001.
• Assistentti: TkL Tommi Junttila
• Materiaali:
  • Henrik Reif Andersen, An Introduction to Binary Decision Diagrams.
  • Jørn Lind-Nielsen, Verification of Large State/Event Systems, Ph.D. dissertation at Department of Information Technology, Technical University of Denmark, Lyngby, Denmark, May 2000.
  • Poul F. Williams Formal Verification Based on Boolean Expression Diagrams, Ph.D. dissertation at Department of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000.
  • M. Sheeran and Gunnar Stålmarck, A tutorial on Stålmarck's proof procedure for propositional logic, Formal Methods in System Design 16 (2000), 23-58.
  • J.F. Groote and J.P. Warners, The propositional formula checker HeerHugo, Journal of Automated Reasoning 24 (2000), 101-125.
  • A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), number 1579 in LNCS. Springer-Verlag, 1999. [ps.gz]
  • Per Bjesse and Koen Claessen, SAT-based Verification without State Space Traversal. In the Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'00), number 1954 of LNCS, Springer-Verlag, 2000. [ps.gz]
  • Burch et al., Symbolic Model Checking: 10E20 States and Beyond, Information and Computation 98 (1992), 142-170.
• Kurssin ohjelma