TCS / Studies / T-79.185 Verification
Helsinki University of Technology, Laboratory for Theoretical Computer Science

T-79.185 Verification (3 cr) P V

Autumn 2004: Symbolic Model Checking

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 T-79.185 course in Autumn 2004 considers two famous techniques for symbolic model checking: binary decision diagram manipulation and bounded model checking.

Time and place

The course is on Tuesdays at 16–19 in T4.

Teachers

Prerequisites (at least corresponding skills expected)

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.185 can be replaced by taking the course T-79.5302 Symbolic Model Checking.

Presentations

Course material

  • [ACK02] Gilles Audemard, Alessandro Cimatti, Artur Korniłowicz, and Roberto Sebastiani, "Bounded Model Checking for Timed Systems," in Doron A. Peled and Moshe Y. Vardi (Eds.), Formal Techniques for Networked and Distributed Systems — FORTE 2002, 22nd IFIP WG 6.1 International Conference, Houston, TX, USA, November 11–14, 2002, Proceedings, in Lecture Notes in Computer Science, Vol. 2529, Springer-Verlag, Berlin, Germany, 2002, pp. 243–259, http://springerlink.metapress.com/link.asp?id=d955nc3ye3utd76d.
  • [AGD92] Pranav Ashar, Abhijit Ghosh, and Srinivas Devadas, "Boolean Satisfiability and Equivalence Checking Using General Binary Decision Diagrams," Integration, the VLSI Journal, Vol. 13, No. 1, May 1992, pp. 1–16.
  • [BBF01] Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Scnoebelen, and (translated with the help of) Pierre McKenzie, Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, Berlin, Germany, 2001.
  • [BCC99] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Jr., and Yunshan Zhu, "Symbolic Model Checking without BDDs," in W. Rance Cleaveland (II) (Ed.), Tools and Algorithms for the Construction and Analysis of Systems, 5th 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.
  • [BCC03] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Jr., Ofer Strichman, and Yunshan Zhu, "Bounded Model Checking," in Marvin V. Zelkowitz (Ed.), Highly Dependable Software, in Advances in Computers, Vol. 58, Academic Press (an imprint of Elsevier), Amsterdam, The Netherlands, 2003, http://www2.inf.ethz.ch/personal/biere/papers/papers.html.
  • [BHV04] Ahmed Bouajjani, Peter Habermehl, and Tomáš Vojnar, "Abstract Regular Model Checking," in Rajeev Alur and Doron A. Peled (Eds.), Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13–17, 2004, Proceedings, in Lecture Notes in Computer Science, Vol. 3114, Springer-Verlag, Berlin, Germany, 2004, pp. 372–386, http://springerlink.metapress.com/link.asp?id=1npy0qt32fb75c9m.
  • [Bry86] Randal E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677–691.
  • [BW94] Bernard Boigelot and Pierre Wolper, "Symbolic Verification with Periodic Sets," in David L. Dill (Ed.), Computer Aided Verification: 6th International Conference, CAV'94, Stanford, CA, USA, July 21–23, 1994, Proceedings, in Lecture Notes in Computer Science, Vol. 818, Springer-Verlag, Berlin, Germany, 1994, pp. 55–67, http://www.montefiore.ulg.ac.be/%7eboigelot/research/.
  • [CCG02] Alessandro Cimatti, Edmund M. Clarke, Jr., Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella, "NuSMV 2: An OpenSource Tool for Symbolic Model Checking," in Ed Brinksma and Kim Guldstrand Larsen (Eds.), Computer Aided Verification: 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27–31, 2002, Proceedings, in Lecture Notes in Computer Science, Vol. 2404, Springer-Verlag, Berlin, Germany, 2002, pp. 359–364, http://springerlink.metapress.com/link.asp?id=7hrq3m38utrrgywb.
  • [CCK04] Roberto Cavada, Alessandro Cimatti, Gavin Keighren, Emmanuele Olivetti, Marco Pistore, and Marco Roveri, NuSMV 2.2 Tutorial, Istituto per la Ricerca Scientifica e Tecnologica, Istituto Trentino di Cultura, Loc. Panté di Povo, Trento, Italy, 2004, http://nusmv.irst.itc.it/NuSMV/tutorial/.
  • [CEP02] Jean-Michel Couvreur, Emmanuelle Encrenaz, Emmanuel Paviot-Adet, Denis Poitrenaud, and Pierre-André Wacrenier, "Data Decision Diagrams for Petri Net Analysis," in Javier Esparza and Charles Lakos (Eds.), Application and Theory of Petri Nets 2002: 23rd International Conference, ICATPN 2002, Adelaide, Australia, June 24–30, 2002, Proceedings, in Lecture Notes in Computer Science, Vol. 2360, Springer-Verlag, Berlin, Germany, 2002, pp. 101–120, http://springerlink.metapress.com/link.asp?id=5tanmq4802d5q29d.
  • [CGP99] Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Model Checking, The MIT Press, Cambridge, MA, USA, 1999.
  • DIM04] Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli, "Bounded Probabilistic Model Checking with the Murφ Verifier," in Alan J. Hu and Andrew K. Martin (Eds.), Formal Methods in Computer-Aided Design, 5th 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. 214–229, http://springerlink.metapress.com/link.asp?id=h9jebhna84aj6ktl.
  • [Eis02] Cindy Eisner, "Using Symbolic CTL Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard," International Journal on Software Tools for Technology Transfer, Vol. 4, No. 1, October 2002, pp. 107–124, http://springerlink.metapress.com/link.asp?id=xuylfg2hywr7u5qu.
  • [ES03] 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, 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.
  • [HJ94] Hans Hansson and Bengt Jonsson, "A Logic for Reasoning about Time and Reliability," Formal Aspects of Computing, Vol. 6, No. 5, September–October 1994, pp. 512–535.
  • [HWA99] Henrik Hulgaard, Poul Frederick Williams, and Henrik Reif Andersen, "Equivalence Checking of Combinational Circuits Using Boolean Expression Diagrams," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 18, No. 7, July 1999, pp. 903–917, http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=16705&puNumber=43.
  • [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.
  • [JMM03] Chris Jefferson, Angela Miguel, Ian Miguel, and Armagan Tarim, "Modelling and Solving English Peg Solitaire," in Michel Gendreau, Gilles Pesant, and Louis-Martin Rousseau (Eds.), Proceedings of the 5th International Workshop on the Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems, CP-AI-OR'03, Montréal, Canada, May 8–10, 2003, pp. 261–275, http://www.crt.umontreal.ca/cpaior/liste.htm. (This paper was attached in the description of the NuSMV part of the T-79.185 Autumn 2004 project.)
  • [KZC00] Priyank Kalla, Zhihong Zeng, Maciej J. Ciesielski, and Chilai Huang, "A BDD-Based Satisfiability Infrastructure Using the Unate Recursive Paradigm," in Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2000, Paris, France, March 27–30, 2000, IEEE Computer Society Press, Los Alamitos, CA, USA, 2000, pp. 232–236, http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=18074&page=2 and http://portal.acm.org/citation.cfm?id=343769.
  • [LBH04] Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila, "Simple Bounded LTL Model Checking," in Alan J. Hu and Andrew K. Martin (Eds.), Formal Methods in Computer-Aided Design, 5th 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.
  • [PC98] Enric Pastor and Jordi Cortadella, "Efficient Encoding Schemes for Symbolic Analysis of Petri Nets," in Proceedings of the Conference on Design, Automation and Test in Europe, DATE'98, Paris, France, February 23–26, 1998, IEEE Computer Society Press, Los Alamitos, CA, USA, 1998, pp. 790–795, http://ieeexplore.ieee.org/xpl/tocresult.jsp?isNumber=14300&page=7 and http://portal.acm.org/citation.cfm?id=368416.
  • [Sor023] Maria Sorea, "Bounded Model Checking for Timed Automata," in Walter Vogler and Kim Guldstrand Larsen (Eds.), Proceedings of the 3rd International Workshop on Models for Time-Critical Systems, MTCS'02, Brno, Czech Republic, August 24, 2002, in Electronic Notes in Theoretical Computer Science, Vol. 68, No. 5, Elsevier, Amsterdam, The Netherlands, 2002 or 2003, http://dx.doi.org/10.1016/S1571-0661(04)80523-1.
  • [Str04] Ofer Strichman, "Accelerating Bounded Model Checking of Safety Properties," Formal Methods in System Design, Vol. 24., No. 1, January 2004, pp. 5–24, http://springerlink.metapress.com/link.asp?id=x8l06n1h3903568r.
  • [TIP04] Yann Thierry-Mieg, Jean-Michel Ilié, and Denis Poitrenaud, "A Symbolic Symbolic State Space Representation," in David de Frutos-Escrig and Manuel Núñez (Eds.), Formal Techniques for Networked and Distributed Systems — FORTE 2004, 24th IFIP WG 6.1 International Conference, Madrid, Spain, September 27–30, 2004, Proceedings, in Lecture Notes in Computer Science, Vol. 3235, Springer-Verlag, Berlin, Germany, 2004, pp. 276–291, http://springerlink.metapress.com/link.asp?id=h827jgd7617gxnjg.
  • [WAH03] Poul Frederick Williams, Henrik Reif Andersen, and Henrik Hulgaard, "Satisfiability Checking Using Boolean Expression Diagrams," International Journal on Software Tools for Technology Transfer, Vol. 5, No. 1, November 2003, pp. 4–14, http://springerlink.metapress.com/link.asp?id=he3q4p2q1ab82dd0.
  • [YHT96] Tomohiro Yoneda, Hideyuki Hatori, Atsushi Takahara, and Shin-ichi Minato, "BDDs vs. Zero-Suppressed BDDs: for CTL Symbolic Model Checking of Petri Nets," in Mandayam K. Srivas and Albert John Camilleri (Eds.), Formal Methods in Computer-Aided Design, 1st International Conference, FMCAD'96, Palo Alto, CA, USA, November 6–8, 1996, Proceedings, in Lecture Notes in Computer Science, Vol. 1166, Springer-Verlag, Berlin, Germany, 1996, pp. 435–449, http://yoneda-www.cs.titech.ac.jp/Papers/bdd-e.htm.

T-79.185 in the past

Autumn 2003, Autumn 2002, Autumn 2001, Autumn 2000.

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 28 March 2006.