We propose a novel approach to locate errors in complex counterexample of safety property. Our approach measures the distance between two state transition traces with difference of their control flow. With respect to this distance metrics, our approach search for a witness as near as possible to the counterexample. Then we can obtain the set of control flow predicates with difference assignment in witness and counterexample. Run this witness-searching algorithm iteratively, we can then obtain a predicate list with priority. A predicate with higher priority means that this predicate is more likely the actual error. Experiment result shows that our approach is highly accurate. © Springer-Verlag 2004.
CITATION STYLE
Shen, G., Qin, Y., & Li, S. (2004). Localizing Errors in Counterexample with Iteratively Witness Searching. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3299, 456–469. https://doi.org/10.1007/978-3-540-30476-0_37
Mendeley helps you to discover research relevant for your work.