Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Shen, S., Qin, Y., Li, S.: Bug Localization of Hardware System with Control Flow Distance Minimization. In: 13th IEEE International Workshop on Logic and Synthesis (IWLS 2004), Temecula, California, USA, (June 2-4, 2004) (accepted)
Shen, S., Qin, Y., Li, S.: Debugging Complex Counterexample of Hardware System using Control Flow Distance Metrics. In: 47rd IEEE Midwest Symposium on Circuits and Systems(MWSCAS 2004), Hiroshima, Japan (July 25-28, 2004) (accpeted)
Ravi, K., Somenzi, F.: Minimal Assignments for Bounded Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (March-April 2004)
Groce, A., Kroening, D., Lerda, F.: Understanding Counterexamples with explain. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 453–456. Springer, Heidelberg (2004)
Ball, T., Naik, M., Rajamani, S.: From Symptom to Cause: Localizing Errors in Counterexample Traces. In: Proceedings of ACM Symposium on Principles of Programming Languages (POPL 2003), New Orleans, LA (January 2003)
Lewis, D.: Causation. Journal of Philosophy 70, 556–567 (1973)
Renieris, M., Reiss, S.: fault localization with nearest neighbor queries. In: Automatic Software Engineering (2003)
Groce, A., Visser, W.: What Went Wrong: Explaining Counterexamples. In: SPIN Workshop on Model Checking of Software, May 2003, pp. 121–135 (2003)
Groce, A.: Error Explanation with Distance Metrics. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (March-April 2004)
Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 445–458 (2002)
Fey, G., Drechsler, R.: Finding Good Counter-Examples to Aid Design Verification. In: Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003) (2003)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 359. Springer, Heidelberg (2002)
Chechik, M., Gurfinkel, A.: Proof-like counterexamples. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 160–175 (2003)
Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A Backtrack-Search Pseudo- Boolean Solver and Optimizer. In: Symposium on the Theory and Applications of Satisfiability Testing (SAT), Ohio, pp. 346–353 (2002)
Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, p. 292. Springer, Heidelberg (2001)
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic Model Checking using SAT procedures instead of BDDs. In: Proceedings of Design Automation Conference (DAC 1999) (1999)
McMillan, K.L., Schwalbe, J.: Formal verification of the Encore Gigamax cache consistency protocols. In: Int. Symp. on Shared Memory Multiprocessors, Tokyo, Japan, April 2-4, pp. 242–251 (1991)
Tan, L., Cleaveland, R.: Evidence-Based Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002)
Namjoshi, K.: Certifying Model Checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 2. Springer, Heidelberg (2001)
Moskewicz, M., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, Las Vegas, NV, June 2001, pp. 530–535 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shen, S., Qin, Y., Li, S. (2004). Localizing Errors in Counterexample with Iteratively Witness Searching. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_37
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive