Abstract
Model-checking is becoming an accepted technique for debugging hardware and software systems. Debugging is based on the “Check / Analyze / Fix” loop: check the system against a desired property, producing a counterexample when the property fails to hold; analyze the generated counterexample to locate the source of the error; fix the flawed artifact – the property or the model. The success of model-checking non-trivial systems critically depends on making this Check / Analyze / Fix loop as tight as possible. In this paper, we concentrate on the Analyze part of the debugging loop. To this end, we present a framework for generating, structuring and exploring counterexamples either interactively or with the help of user-specified strategies.
Chapter PDF
Similar content being viewed by others
References
Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstraction for Model Checking C Programs. STTT 5(1), 49–58 (2003)
Barner, S., Ben-David, S., Gringauze, A., Sterin, B., Wolfsthal, Y.: An algorithmic approach to design exploration. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 146–162. Springer, Heidelberg (2002)
Chechik, M., Gurfinkel, A., Devereux, B.: χChek: A multi-valued model-checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 505–509. Springer, Heidelberg (2002)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Grumberg, O., McMillan, K.L., Zhao, X.: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. In: Proceedings of DAC 1995, pp. 427–432 (1995)
Clarke, E.M., Lu, Y., Jha, S., Veith, H.: Tree-Like Counterexamples in Model Checking. In: Proceedings of LICS 2002, pp. 19–29 (2002)
Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient debugging in a formal verification environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 275–292. Springer, Heidelberg (2001)
Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Evidence Explorer: A Tool for Exploring Model-Checking Proofs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 215–218. Springer, Heidelberg (2003)
Dong, Y., Ramakrishnan, C.R., Smolka, S.A.: Model Checking and Evidence Exploration. In: Proceedings of ECBS 2003, April 2003, pp. 214–223 (2003)
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of ICSE 1999 (May 1999)
Groce, A., Visser, W.: What Went Wrong: Explaining Counterexamples. In: Proceedings of SPIN Workshop on Model Checking of Software, pp. 121–135 (2003)
Gurfinkel, A., Chechik, M.: Proof-like counter-examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160–175. Springer, Heidelberg (2003)
Namjoshi, K.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 2. Springer, Heidelberg (2001)
Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, p. 292. Springer, Heidelberg (2001)
Plath, M.C., Ryan, M.D.: SFI: A Feature Integration Tool. In: Berghammer, R., Lakhnech, Y. (eds.) Tool Support for System Specification, Development and Verification. Advances in Computer Science, pp. 201–216. Springer, Heidelberg (1999)
Tan, L., Cleaveland, W.R.: Evidence-Based Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chechik, M., Gurfinkel, A. (2005). A Framework for Counterexample Generation and Exploration. In: Cerioli, M. (eds) Fundamental Approaches to Software Engineering. FASE 2005. Lecture Notes in Computer Science, vol 3442. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31984-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-31984-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25420-1
Online ISBN: 978-3-540-31984-9
eBook Packages: Computer ScienceComputer Science (R0)