Morning Master Class, Thursday November 2, 2006
Domain-specific Model Checking with Bogor
Robby (Kansas State University)

Model checking has proven to be an effective technology for
verification and debugging in hardware and more recently in software
domains. We believe that for model checking technology to be
effectively applied to software, model checking tools must directly
support language constructs found in modern object-oriented languages
like Java and C# and underlying checking algorithms must make use of
sophisticated analyses similar to those found in optimizing compilers
to reduce model checking costs. Moreover, 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.

The Bogor model checking framework is an extensible and highly modular
explicit-state model checking framework that aims to (a) overcome
limitations of existing model checking tools that fail to provide
direct support modeling software, and to (b) enable more effective
incorporation of domain knowledge into verification models and
associated model checking algorithms and optimizations.  This lecture
will cover topics related to Bogor's design principles, graphical user
interface and visualizations, internal architecture and APIs, working
with architectural elements to create customized domain-specific
model-checking engines, and example deployments of Bogor in large
scale development/verification environments.