Model Checking and Evidence Exploration

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


We present an algebraic framework for evidence exploration: the process of interpreting, manipulating, and 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. Evidence exploration allows users to explore evidence through smaller, manageable views, which are definable in relational graph algebra, a natural extension of relational algebra to graph structures such as model-checking evidence. We illustrate the utility of our approach by applying the Evidence Explorer, our tool implementation of the evidence-exploration framework, to the Java meta-locking algorithm, a highly optimized technique deployed by the Java Virtual Machine to ensure mutually exclusive access to object monitor queues by threads.

Bibtex Entry:

author = {Yifei Dong and  C. R. Ramakrishnan and  Scott A. Smolka},
title = {Model Checking and Evidence Exploration},
booktitle = {IEEE Conference and Workshops on Engineering Computer Based Systems},
address = {Huntsville, Alabama},
publisher = {IEEE},
pages = {214--223},
year = {2003}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan