Mini-Tutorials

Domain-specific Model Checking Using The Bogor Framework

Wednesday, September 20, 14:00-15:30
Room: Conference Room 3 & 4 (2F)

Abstract
Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools. To overcome limitations of existing tools which tend to be monolithic and non-extensible, we have developed an extensible and customizable model checking framework called Bogor. In this tutorial, we give an overview of (a) Bogor's direct support for modeling object-oriented designs and implementations, (b) its facilities for extending and customizing its modeling language and algorithms to create domain-specific model checking engines, and (c) pedagogical materials that we have developed to describe the construction of model checking tools built on top of the Bogor infrastructure.

Testing Tools and Techniques: A Mini-Tutorial on Evaluation Methods for ASE

Thursday, September 21, 14:00-15:30
Room: Hitotsubashi Memorial Hall

Instructor
Janice Singer, National Research Council, Canada

Abstract
Ever wonder how your tool would fare in the "real world"? Think your tool excels where others have failed? Is your tool better than a software developer? How can your tool help a software developer? Have you asked these kinds of questions before? If so, then this mini-tutorial is focused on your needs. In the minitutorial, I will go over the basics of tool evaluation from the beginning to end, from ethics to theory to analysis. Both qualitative and quantitative approaches will be covered.