TCS /
Teaching / Tik-79.298
Tik-79.298 Digitaalisten järjestelmien lisensiaattikurssi
kevät 2001
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
Viimeksi päivitetty: Jan 15, 2001
Ilkka.Niemela@hut.fi