Published Articles >> Table of Contents >> Abstract

17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)   p. 19
Tree-Like Counterexamples in Model Checking
Edmund Clarke, Carnegie Mellon University
Somesh Jha, University of Wisconsin
Yuan Lu, Broadcom COM
Helmut Veith, Technische Universität Wien

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029814
Send link to a friend

Abstract
Counterexamples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework for counterexamples. The paper has three main contributions: (i) We determine the general form of ACTL counterexamples. To this end, we investigate the notion of counterexample and show that a large class of temporal logics beyond ACTL admits counterexamples with a simple tree-like transition relation. We show that the existence of tree-like counterexamples is related to a universal fragment of extended branching time logic based on !
Back to Top Additional Information
Citation:  Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith, "Tree-Like Counterexamples in Model Checking," lics, p. 19,  17th Annual IEEE Symposium on Logic in Computer Science (LICS'02),  2002