This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
Tree-Like Counterexamples in Model Checking
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
Edmund Clarke, Carnegie Mellon University
Somesh Jha, University of Wisconsin
Yuan Lu, Broadcom COM
Helmut Veith, Technische Universität Wien
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 !
Citation:
Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith, "Tree-Like Counterexamples in Model Checking," lics, pp.19, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.