Abstract
We present the Evidence Explorer (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 [3], views are definable in relational graph algebra, a natural extension of relational algebra to graph structures such as model-checking evidence.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Basu, S., Smolka, S.A., Ward, O.R.: Model checking the Java Meta-Locking algorithm. In: ECBS 2000, pp. 342–350 (2000)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods in System Design 18(2), 141–163 (2001)
Dong, Y., Ramakrishnan, C., Smolka, S.A.: Model checking and evidence exploration. In: ECBS 2003, pp. 214–223 (2003)
Krasner, G., Pope, S.: A description of the model-view-controller user interface paradigm in the Smalltalk-80 system. J. Object Oriented Prog. 1(3), 26–49 (1988)
Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)
Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001)
Ramakrishnan, C., Ramakrishnan, I., Smolka, S.A., Dong, Y., Du, X., Roychoudhury, A., Venkatakrishnan, V.: XMC: A logic-programming-based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 576–580. Springer, Heidelberg (2000)
Tan, L., Cleaveland, W.R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dong, Y., Ramakrishnan, C.R., Smolka, S.A. (2003). Evidence Explorer: A Tool for Exploring Model-Checking Proofs. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive