Evidence Exploration for Model Checking

			       Yifei Dong

Formal methods are mathematically based languages that form the basis
for techniques and and tools for specifying and verifying systems.  In
theory, compared with traditional "informal" specification and
verification, formal methods enable developers design and check their
systems more rigorously.  In practice, however, apart from a few success
stories especially the increasing use in electronic design automation
(EDA), formal methods have not been widely accepted by computer
practitioners.  This gap is in part due to the perceived lack of
usability in formal verification techniques.

In this talk, I will discuss the usability problems in the latter stages
of model checking: manipulating and interpreting the output of a model
checker, in particular its proof structure, or evidence.  Due to the
sheer size of such evidence, single-step traversal is prohibitive and
smarter exploration methods are required.  I present an algebraic
framework for evidence exploration that allows users to explore evidence
through smaller, manageable views.  The views are definable in
relational graph algebra, a natural extension of relational algebra to
graph structures such as model-checking evidence.  The effectiveness of
this framework is demonstrated by my prototype tool, the Evidence
Explorer, which allow a user to quickly hone in on the portions of
interest of model-checking evidence from a real-life application.

At the end of the talk, I will briefly introduce my ongoing research and
future plan on formal methods as well as their theoretical foundation
and practical applications in software engineering, programming
languages, and communication protocols.