T-79.5302 Symbolic Model Checking (4 cr) P

Autumn 2005

Symbolic model checking made a breakthrough in hardware verification in the beginning of 1990's and has since then 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.

Time and place

The course is on Thursdays at 17–20 in TB353. The course starts on September 15.

Teachers

• Tommi Junttila (D.Sc. (Tech.)) and
• Kimmo Varpaaniemi (Docent, D.Sc. (Tech.)).

How to pass

In order to pass, a student must give presentations in the seminar and do a small project. The number of presentations and the length of a single presentation depend on the number of participants. As expressed by the Language characterization below, it is technically possible to compensate presentations e.g. by writing essays. However, the course staff makes decisions on potential compensations case by case. The project is a single-person project unless stated otherwise. The course grade is determined by the quality of the work done in the seminar and in the project.

Language

The seminar is arranged in Finnish, but a student can give his/her presentation and write the project documents in English, too. Skipping presentations given in Finnish/English can be compensated by other means, e.g. by writing essays.

Note

The course T-79.5302 replaces either the course T-79.185 Verification or the course T-79.193 Formal Description Techniques for Concurrent Systems.

Presentations

• Sep 15 / the course staff: a brief introduction.
• Sep 22 / Jan Lönnberg: [CGP99: Ch. 2 & 3] + [McM93: Ch. 2].
• Sep 29 / Topi Pohjolainen: [Hel97: Ch. 3].
• Oct 6 / Vesa Ojala: [Bry01].
• Oct 6 / Jan Lönnberg: [McM93: Ch. 3].
• Oct 13 / Joosu Terhivuo: [McM93: Ch. 4 & 5].
• Oct 20 / Jan Lönnberg: [BCC99] + [BCR99].
• Nov 3 / Joosu Terhivuo: [ES03].
• Nov 10 / Antti Rusanen: [LBH04] + [LBH05].
• Nov 17 / Joosu Terhivuo: [JHN05].

Course material so far

• [BCC99] Armin Biere, Alessandro Cimatti, Edmund Melson Clarke, Jr., and Yunshan Zhu, "Symbolic Model Checking without BDDs," in Walter Rance Cleaveland II (Ed.), Tools and Algorithms for the Construction and Analysis of Systems, 5^th International Conference, TACAS'99, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22–28, 1999, Proceedings, in Lecture Notes in Computer Science, Vol. 1579, Springer-Verlag, Berlin, Germany, 1999, pp. 193–207, http://springerlink.metapress.com/link.asp?id=vf286k9mq0jp05dh.
• [BCR99] Armin Biere, Edmund Melson Clarke, Jr., Richard Raimi, and Yunshan Zhu, "Verifying Safety Properties of PowerPC™ MicroProcessor Using Symbolic Model Checking without BDDs," in Nicolas Halbwachs and Doron Angel Peled (Eds.), Computer Aided Verification: 11^th International Conference, CAV'99, Trento, Italy, July 6–10, 1999, Proceedings, in Lecture Notes in Computer Science, Vol. 1633, Springer-Verlag, Berlin, Germany, 1999, pp. 60–71, http://springerlink.metapress.com/link.asp?id=h5vnx8lyeaa0xtnv.
• [Bry86] Randal Everitt Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677–691.
• [Bry01] Randal Everitt Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," a revised electronic version of [Bry86], School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA, November 2001, http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf.
• [CGP99] Edmund Melson Clarke, Jr., Orna Grumberg, and Doron Angel Peled, Model Checking, The MIT Press, Cambridge, MA, USA, 1999.
• [ES03] 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, in Electronic Notes in Theoretical Computer Science, Vol. 89, No. 4, Elsevier, Amsterdam, The Netherlands, 2003, pp. 543–560, http://dx.doi.org/10.1016/S1571-0661(05)82542-3.
• [Hel97] Keijo Heljanko, Model Checking the Branching Time Temporal Logic CTL, Research Report A45, Digital Systems Laboratory, Helsinki University of Technology, Espoo, Finland, May 1997, http://www.tcs.hut.fi/Publications/bibdb/HUT-TCS-A45.ps.
• [JHN05] 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, http://springerlink.metapress.com/link.asp?id=wuuqg7mpyn8xbm6g.
• [LBH04] Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila, "Simple Bounded LTL Model Checking," in Alan John Hu and Andrew Kennneth Martin (Eds.), Formal Methods in Computer-Aided Design, 5^th International Conference, FMCAD 2004, Austin, TX, USA, November 15–17, 2004, Proceedings, in Lecture Notes in Computer Science, Vol. 3312, Springer-Verlag, Berlin, Germany, 2004, pp. 186–200, http://springerlink.metapress.com/link.asp?id=a1jnfcb7q9knc1q1.
• [LBH05] 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, 6^th International Conference, VMCAI 2005, Paris, France, January 17–19, 2005, Proceedings, in Lecture Notes in Computer Science, Vol. 3385, Springer-Verlag, Berlin, Germany, 2005, pp. 380–395, http://springerlink.metapress.com/link.asp?id=p4e4t16wk8uyqjgk.
• [McM93] Kenneth Lauchlin McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, USA, 1993.