FM 2006

August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006


Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006

Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chair

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel

T6 Model Checking: From Hardware to Software
Marsha Chechik
Arie Gurfinkel
University of Toronto, Canada
August 22, 2006
2:00-5:30, 1/2hr break at 3:30
ITB 225
Half-day (afternoon) Slides, these will also be made available in printed form.


Over the past twenty years, model-checking has emerged as the most prominent automated reasoning technique, which promises push-button automation. Correctness is specified as a set of properties expressed in temporal logic; a model-checker either establishes that the property holds, or returns a counterexample explaining the reason for the failure. Model-checking is ultimately a state-exploration technique, and as such, suffers from a state explosion problem: the statespace of the model is exponentially larger than its textual description.

Modern approaches to model-checking combine a variety of techniques: efficient data structures, decision procedures, symbolic reasoning, abstraction, and many others.

The goal of the tutorial is to survey classical and emerging model- checking techniques for checking hardware and software, with the aim of achieving understanding the effectiveness and the limitations of the underlying technology.


- Specifying correctness of artifacts
- Modeling formalisms
- Major algorithms and underlying technology
- User issues: understanding model-checking feedback
- Creating effective abstractions
- Model-checking software


The tutorial assumes no prior experience with model-checkers, and due to the breadth of topics covered, it should be of interest to a variety of participants, from industry and academia.

Biography of Tutors:

Marsha Chechik received her Ph.D. from the University of Maryland, and is currently an associate professor in the Department of Computer Science at the University of Toronto, cross-appointed to the Department of Electrical and Computer Engineering. Prof. Chechik's research interests are mainly in construction and application of automated reasoning techniques to improve the quality of software. She has authored around 50 papers in formal methods, software specification and verification, and requirements engineering. She is an associate editor of IEEE Transactions on Software Engineering and has served on program committees of numerous international conferences. Prof. Chechik has been studying and teaching model-checking for the past 10 years.

Arie Gurfinkel is a PhD student in the Department of Computer Science at the University of Toronto and will be graduating in the summer of 2006. He has received a B.Sc. and a M.Sc. degrees in computer science from the University of Toronto, in 2000 and 2003, respectively. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated techniques for program verification. Arie has received an NSERC Postgraduate Scholarship in 2003, and an IBM Ph.D. Fellowship in 2004. In the summer of 2005, he completed an internship at IBM CAS Toronto, where he worked on integrating a software model-checker YASM within the Eclipse IDE, and explored static and dynamic approaches for analysis of web services.