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.

Current

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

General

• 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: http://www.tcs.hut.fi/Studies/T-79.5302/

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
  Material:
  • 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
  Material:
  • Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677-691.
  • Lecture notes on BDDs by Henrik Reif Andersen.
  • Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys, Vol. 24, Issue 3 , September 1992, pp. 293-318.
• Oct 2 / Jani Lampinen : Symbolic model checking of CTL
  Material:
  • 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
  Material:
  • Chapters 3 and 4 of Kenneth L. McMillan, Symbolic Model Checking, An approach to the state explosion problem Technical Report CMU-CS-92-131, Carnegie Mellon University, 1992.
• Oct 16 / Jussi Lahtinen : BDD-based symbolic model checking of LTL
  Material:
  • 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
  Material:
  • Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Jr., and Yunshan Zhu, Symbolic Model Checking without BDDs, in Rance Cleaveland (Ed.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), Lecture Notes in Computer Science, Vol. 1579, Springer, 1999, pp. 193-207.
  • Armin Biere, Edmund M. Clarke, Jr., Richard Raimi, and Yunshan Zhu, Verifying Safety Properties of PowerPC™ MicroProcessor Using Symbolic Model Checking without BDDs, in Nicolas Halbwachs and Doron Peled (Eds.), Computer Aided Verification (CAV'99), Lecture Notes in Computer Science, Vol. 1633, Springer, 1999, pp. 60-71.
• Oct 30 : no seminar, examination period
• Nov 6 / Mikko Lahola : Compact encodings for bounded model checking of LTL
  Material:
  • 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
  Material:
  • 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 1^st 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
  Material:
  • 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
  Material:
  • G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani, Bounded Model Checking for Timed Systems, in D. A. Peled and M.Y. Vardi (Eds.), Formal Techniques for Networked and Distributed Sytems (FORTE 2002), Lecture Notes in Computer Science, Vol. 2592, Springer, 2002, pp. 243-259.
  • Maria Sorea, Bounded Model CHecking for Timed Automata, Electronic Notes in Theoretical Computer Science, Vol. 68, No. 5, Elsevier, 2002, pp. 116-134.
  • Gilles Audemard, Marco Bozzano, Alessandro Cimatti, and Roberto Sebastiani, Verifying Industrial Hybrid Systems with MathSAT, Electronic Notes in Theoretical Computer Science, Vol. 199, Elsevier, 2005,pp. 17-25.
• Dec 4 / Siert Wieringa : Interpolant-based methods
  Material:
  • K.L. McMillan, Interpolation and SAT-Based Model Checking, in CAV'03, Lecture Notes in Computer Science, Vol. 2725, Springer, 2003, pp. 1-13.
  • K.L. McMillan, Applications of Graig Interpolants in Model Checking, in TACAS'05, Lecture Notes in Computer Science, Vol. 3440, Springer, 2005, pp. 1-12.
• Dec 11 / N.N. : to be announced
  Material:
  • To be announced.