A Framework for Counterexample Generation and Exploration

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.

• Type: Conference
• Year: 2005
• Where: FASE
• Authors: Marsha Chechik, Arie Gurfinkel
• Keywords: Counterexamples, Debugging, FASE 2005, Model-checking Non-trivial Systems, Software Engineering