**Advanced Tutorial at ACSD 2006 / Petri Nets 2006**

List of topics to covered:

- Bounded Model Checking Basics
- Encoding a Transition Relation - Exploiting Concurrency
- Combining Partial Order Methods with LTL Model Checking
- Encoding LTL Properties
- Incremental Bounded Model Checking
- Making Bounded LTL Model Checking Complete
- Encoding PLTL Properties

Schedule:

- 9:00 - 10:30 Tutorial part 1 - Keijo Heljanko: BMC basics
- 10:30 - 11:00 Coffee break
- 11:00 - 12:30 Tutorial part 2 - Keijo Heljanko: Exploiting concurrency in BMC
- 12:30 - 13:30 Lunch
- 13:30 - 15:00 Tutorial part 3 - Tommi Junttila: Encoding LTL in BMC
- 15:00 - 15:30 Coffee break
- 15:30 - 17:00 Tutorial part 4 - Tommi Junttila: Incremental and complete BMC, PLTL

Tutorial material:

- Slides for tutorial parts 1-2 as PDF, as gzipped Postscript, 4 slides per page.
- Slides for tutorial parts 3-4 as PDF, as gzipped Postscript, 4 slides per page.
- Demo for tutorial parts 1-2 as PDF, as gzipped Postscript, 4 slides per page.
- Nets, circuits, and tools used in the demo for parts 1-2: README-demo.txt, Demo nets, circuits, and BMC tools (18 Megabytes).

Keijo Heljanko
Helsinki University of Technology (TKK) Laboratory for Theoretical Computer Science P.O. Box 5400 FI-02015 TKK Finland |

Tommi Junttila
Helsinki University of Technology (TKK) Laboratory for Theoretical Computer Science P.O. Box 5400 FI-02015 TKK Finland |

ACSD 2006 / Petri nets 2006 homepage

- Clarke, E. M., Grumberg, O., and Peled, D. A.: Model Checking, MIT press, 2000.
- Biere, A., Cimatti, A., Clarke, E. and Zhu, Y.: Symbolic Model Checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), pages 193-207, Lecture notes in Computer Science 1579, Springer-Verlag, 1999.
- Keijo Heljanko. Bounded reachability checking with process semantics. In Kim Guldstrand Larsen and Mogens Nielsen, editors, Proceedings of the 12th International Conference on Concurrency Theory (Concur' 2001), volume 2154 of Lecture Notes in Computer Science, pages 218-232, Aalborg, Denmark, August 2001. Springer-Verlag.
- Keijo Heljanko, Tommi Junttila, and Timo Latvala. Incremental and complete bounded model checking for full PLTL. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'2005), Lecture Notes in Computer Science 3576, pages 98-111, Edinburgh, Scotland, United Kingdom, to appear. Springer-Verlag.
- Keijo Heljanko and Ilkka Niemelä. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming, 3(4&5): 519-550, 2003.
- Toni Jussila, Keijo Heljanko, and Ilkka Niemelä. BMC via on-the-fly determinization. STTT - International Journal on Software Tools for Technology Transfer, 7(2):89-101, 2005.
- Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan Hu and Andy Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 186-200. Springer-Verlag, November 2004.
- Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple is better: Efficient bounded model checking for past LTL. In Radia Cousot, editor, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'2005), volume 3385 of Lecture Notes in Computer Science, pages 380-395, Paris, France, January 2005. Springer-Verlag.

Last modified: Fri Mon 19 2005 |