TCS / Studies / T-79.5302 Symbolic Model Checking
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

T-79.5302 Symbolic Model Checking (4 cr) P

Autumn 2007 (periods I and II)

Model checking is a method for analyzing whether the dynamic behavior of a hardware or software system meets its specification. It has been succesfully applied in, for example, validating communication protocols, verifying components of microprocessor designs, and finding bugs in device drivers. In a way, model checking can be seen as a way of performing exhaustive testing. Symbolic model checking is a particular form of model checking in which the state and transition information of the system under consideration are represented and manipulated symbolically by means of logical formulae. The goal of this is to cope with the inherent high computational complexity of model checking. Since its invention in the beginning of 1990's, symbolic model checking has made a breakthrough in hardware verification and has been increasingly popular in software verification, too. The course T-79.5302 considers two famous techniques for symbolic model checking: binary decision diagram manipulation and bounded model checking.


  • [3 Sep 2007] First meeting on Tuesday 11th of September, room TB353.


  • Coordinator: Dr. Tommi Junttila
  • Seminar meetings: On Tuesdays from 16.15 to 19.00 in the seminar room TB353 of the computer science building (T-talo). The first meeting will be on Tuesday 11th of September.
  • Prerequisites: Basic knowledge of problem representations and logic (T-79.1001, T-79.3001); parallel and distributed systems (T-79.4301); basic knowledge on programming languages (Java, C, etc.)
  • Requirements for passing the course:
    • Attending the seminars.
    • Giving seminar presentations. The length of a presentation should be 60-90 minutes. The number of presentations depend on the number of participants.
    • Making small exercise projects. The projects are single-person projects.
    The course grade is determined by the quality of the work done in the seminar and in the projects.
  • Course web site:

Schedule (tentative)

  • Sep 11 / the course staff: a brief introduction
  • Sep 18 / Kari Kähkönen : Kripke structures, modeling systems, specifying properties with temporal logics CTL and LTL
    • Chapters 2 and 3 of Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Model Checking, The MIT Press, Cambridge, MA, USA, 1999.
  • Sep 25 / Timo Lindfors : Boolean function manipulation with Binary decision diagrams
  • Oct 2 / Jani Lampinen : Symbolic model checking of CTL
    • Sections 4.1, 6.1, 6.2, 6.3, and 6.4 of Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Model Checking, The MIT Press, Cambridge, MA, USA, 1999.
    • Possibly some additional supporting material.
  • Oct 9 / Otto Seppälä : The SMV system and a case study
  • Oct 16 / Jussi Lahtinen : BDD-based symbolic model checking of LTL
    • Edmund M. Clarke, Orna Grumberg, and Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Formal Methods in System Design, Vol. 10, pp. 47-71, 1997.
    • Also see Section 6.7 (and compare with Section 4.2) of Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Model Checking, The MIT Press, Cambridge, MA, USA, 1999.
  • Oct 23 / Matti Koskimies : Bounded model checking
  • Oct 30 : no seminar, examination period
  • Nov 6 / Mikko Lahola : Compact encodings for bounded model checking of LTL
    • Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila, Simple Bounded LTL Model Checking, in Alan Hu and Andrew Martin (Eds.), Formal Methods in Computer-Aided Design (FMCAD 2004), Lecture Notes in Computer Science, Vol. 3312, Springer, 2004, pp. 186-200.
    • Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila, Simple Is Better: Efficient Bounded Model Checking for Past LTL, in Radhia Cousot (Ed.), Verification, Model Checking, and Abstract Interpretation (VMCAI 2005), Lecture Notes in Computer Science, Vol. 3385, Springer, 2005, pp. 380-395.
  • Nov 13 / Sami Liedes : SAT-based temporal induction
    The slides of the presentation are available here
    • Mary Sheeran, Satnam Singh, Gunnar Stålmarck: Checking Safety Properties Using Induction and a SAT-Solver, in Warren A. Hunt Jr. and Steven D. Johnson (Eds.), Formal Methods in Computer-Aided Design (FMCAD 2000), Lecture Notes in Computer Science, Vol. 1954, Springer, 2000, pp. 108-125.
    • Niklas Eén and Niklas Sörensson, Temporal Induction by Incremental SAT Solving, in Ofer Strichman and Armin Biere (Eds.), Proceedings of the 1st International Workshop on Bounded Model Checking Methods, BMC'2003, Boulder, CO, USA, July 13, 2003, Electronic Notes in Theoretical Computer Science, Vol. 89, No. 4, Elsevier, Amsterdam, The Netherlands, 2003, pp. 543-560.
  • Nov 20 / Antti Hyvärinen : Exploiting concurrency in bounded model checking
    • Toni Jussila, Keijo Heljanko, and Ilkka Niemelä, BMC via On-the-Fly Determinization, International Journal on Software Tools for Technology Transfer, Vol. 7, No. 2, April 2005, pp. 89-101.
  • Nov 27 / Perttu Halonen : Bounded Model Checking of Timed and Linear Hybrid Systems
  • Dec 4 / Siert Wieringa : Interpolant-based methods
  • Dec 11 / N.N. : to be announced
    • To be announced.

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 15 November 2007.