Model checking and evidence exploration

Yifei Dong; C. R. Ramakrishnan; S. A. Smolka

doi:10.1109/ECBS.2003.1194802

Model checking and evidence exploration

Computer Science

Stony Brook University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

16 Scopus citations

Abstract

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.

Original language	English
Title of host publication	Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	214-223
Number of pages	10
ISBN (Electronic)	0769519172, 9780769519173
DOIs	https://doi.org/10.1109/ECBS.2003.1194802
State	Published - 2003
Event	10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003 - Huntsville, United States Duration: Apr 7 2003 → Apr 10 2003

Publication series

Name	Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003

Conference

Conference	10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003
Country/Territory	United States
City	Huntsville
Period	04/7/03 → 04/10/03

Keywords

Algebra
Computer science
Electronic mail
Formal verification
Java
Logic
Navigation
Switches
Usability
Virtual machining

Access to Document

10.1109/ECBS.2003.1194802

Cite this

Dong, Y., Ramakrishnan, C. R., & Smolka, S. A. (2003). Model checking and evidence exploration. In Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003 (pp. 214-223). Article 1194802 (Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ECBS.2003.1194802

Dong, Yifei ; Ramakrishnan, C. R. ; Smolka, S. A. / Model checking and evidence exploration. Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003. Institute of Electrical and Electronics Engineers Inc., 2003. pp. 214-223 (Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003).

@inproceedings{183cc9f0eeeb438aaa2390b7b7c16afe,

title = "Model checking and evidence exploration",

abstract = "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.",

keywords = "Algebra, Computer science, Electronic mail, Formal verification, Java, Logic, Navigation, Switches, Usability, Virtual machining",

author = "Yifei Dong and Ramakrishnan, \{C. R.\} and Smolka, \{S. A.\}",

note = "Publisher Copyright: {\textcopyright} 2003 IEEE.; 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003 ; Conference date: 07-04-2003 Through 10-04-2003",

year = "2003",

doi = "10.1109/ECBS.2003.1194802",

language = "English",

series = "Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "214--223",

booktitle = "Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003",

}

Dong, Y, Ramakrishnan, CR & Smolka, SA 2003, Model checking and evidence exploration. in Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003., 1194802, Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003, Institute of Electrical and Electronics Engineers Inc., pp. 214-223, 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003, Huntsville, United States, 04/7/03. https://doi.org/10.1109/ECBS.2003.1194802

Model checking and evidence exploration. / Dong, Yifei; Ramakrishnan, C. R.; Smolka, S. A.
Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003. Institute of Electrical and Electronics Engineers Inc., 2003. p. 214-223 1194802 (Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Model checking and evidence exploration

AU - Dong, Yifei

AU - Ramakrishnan, C. R.

AU - Smolka, S. A.

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

KW - Algebra

KW - Computer science

KW - Electronic mail

KW - Formal verification

KW - Java

KW - Logic

KW - Navigation

KW - Switches

KW - Usability

KW - Virtual machining

UR - https://www.scopus.com/pages/publications/35248892210

U2 - 10.1109/ECBS.2003.1194802

DO - 10.1109/ECBS.2003.1194802

M3 - Conference contribution

AN - SCOPUS:35248892210

T3 - Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003

SP - 214

EP - 223

BT - Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003

Y2 - 7 April 2003 through 10 April 2003

ER -

Dong Y, Ramakrishnan CR , Smolka SA. Model checking and evidence exploration. In Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003. Institute of Electrical and Electronics Engineers Inc. 2003. p. 214-223. 1194802. (Proceedings - 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, ECBS 2003). doi: 10.1109/ECBS.2003.1194802

Model checking and evidence exploration

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this