Evidence Explorer: A Tool for Exploring Model-Checking Proofs

Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka


We present the Evidence Explorer (See http://www.cs.sunysb.edu/~lmc/ee/), a new tool for assisting users in navigating the proof structure, or evidence, produced by a model checker when attempting to verify a system specification for a temporal-logic property. Due to the sheer size of such evidence, single-step traversal is prohibitive and smarter exploration methods are required. The Evidence Explorer enables users to explore evidence through a collection of orthogonal but coordinated views. These views allow one to quickly ascertain the overall perception of evidence through consistent visual cues, and easily locate interesting regions by simple drill-down operations. As described in our earlier paper (appeared in ECBS03), views are definable in relational graph algebra, a natural extension of relational algebra to graph structures such as model-checking evidence.

Our experience in using the Evidence Explorer on several case studies of real-life systems indicates that its use can lead to increased productivity due to shortened evidence traversal time. For example, in the case of formally verifying the Sun Microsystems Java meta-locking algorithm for mutual exclusion and freedom from lockout, we had to spend nearly an hour to expand and step through one of the generated model-checking proofs using a standard tree browser. With the Evidence Explorer, we not only cut the process to only a couple of minutes but also were able to recognize the key elements instantly and experiment with the specification via more frequent modifications.

Bibtex Entry:

author = {Yifei Dong and  C. R. Ramakrishnan and  Scott A. Smolka},
title = {Evidence Explorer: A Tool for Exploring Model-Checking Proofs},
booktitle = {Fifteenth International Conference on Computer Aided Verification ({CAV})},
address = {Boulder, Colorado},
month = {July},
series = {Lecture Notes in Computer Science},
volume = {2725},
publisher = {Springer},
pages = {215--218},
year = {2003}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan