T6 Model Checking: From Hardware to Software
|
Tutors: |
Marsha Chechik
Arie Gurfinkel |
Affiliation: |
University of Toronto, Canada |
Date: |
August 22, 2006 |
Time: |
2:00-5:30, 1/2hr break at 3:30 |
Location: |
ITB 225 |
Format: |
Half-day (afternoon)
Slides , these will also be made available in printed form. |
| |
Topic:
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.
|
Objective:
- Specifying correctness of artifacts
- Modeling formalisms
- Major algorithms and underlying technology
- User issues: understanding model-checking feedback
- Creating effective abstractions
- Model-checking software
|
Prerequisites:
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.
|
