
T79.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 T79.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 (Ttalo).
The first meeting will be on Tuesday 11th of September.
 Prerequisites:
Basic knowledge of problem representations and logic
(T79.1001, T79.3001);
parallel and distributed systems (T79.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 6090 minutes.
The number of presentations depend on the number of participants.

Making small exercise projects.
The projects are singleperson 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/T79.5302/

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,
GraphBased Algorithms for Boolean Function Manipulation,
IEEE Transactions on Computers,
Vol. C35, No. 8, August 1986,
pp. 677691.

Lecture notes on BDDs by
Henrik Reif Andersen.

Randal E. Bryant,
Symbolic Boolean manipulation with ordered binarydecision diagrams,
ACM Computing Surveys,
Vol. 24, Issue 3 , September 1992, pp. 293318.

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:

Oct 16 / Jussi Lahtinen
: BDDbased 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. 4771, 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. 193207.

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. 6071.

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 ComputerAided Design (FMCAD 2004),
Lecture Notes in Computer Science,
Vol. 3312, Springer, 2004,
pp. 186200.

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. 380395.

Nov 13 / Sami Liedes
: SATbased 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 SATSolver,
in Warren A. Hunt Jr. and Steven D. Johnson (Eds.),
Formal Methods in ComputerAided Design (FMCAD 2000),
Lecture Notes in Computer Science, Vol. 1954, Springer, 2000, pp. 108125.

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. 543560.

Nov 20 / Antti Hyvärinen
: Exploiting concurrency in bounded model checking
Material:

Toni Jussila, Keijo Heljanko, and Ilkka Niemelä,
BMC via OntheFly Determinization,
International Journal on Software Tools for Technology Transfer,
Vol. 7, No. 2, April 2005, pp. 89101.

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. 243259.

Maria Sorea,
Bounded Model CHecking for Timed Automata,
Electronic Notes in Theoretical Computer Science,
Vol. 68, No. 5, Elsevier, 2002, pp. 116134.

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. 1725.

Dec 4 / Siert Wieringa
: Interpolantbased methods
Material:

K.L. McMillan,
Interpolation and SATBased Model Checking,
in CAV'03,
Lecture Notes in Computer Science, Vol. 2725, Springer, 2003, pp. 113.

K.L. McMillan,
Applications of Graig Interpolants in Model Checking,
in TACAS'05,
Lecture Notes in Computer Science, Vol. 3440, Springer, 2005, pp. 112.

Dec 11 / N.N.
: to be announced
Material:
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 15 November 2007.
