|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| 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
| ASCII Text | x | ||
| Edmund Clarke, Somesh Jha, Yuan Lu, Helmut Veith, "Tree-Like Counterexamples in Model Checking," Logic in Computer Science, Symposium on, pp. 19, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2002.1029814, author = {Edmund Clarke and Somesh Jha and Yuan Lu and Helmut Veith}, title = {Tree-Like Counterexamples in Model Checking}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2002}, issn = {1043-6871}, pages = {19}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029814}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Tree-Like Counterexamples in Model Checking SN - 1043-6871 SP EP A1 - Edmund Clarke, A1 - Somesh Jha, A1 - Yuan Lu, A1 - Helmut Veith, PY - 2002 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
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.
