A Framework for Counterexample Generation and Exploration

10 years 9 months ago
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.
Marsha Chechik, Arie Gurfinkel
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FASE
Authors Marsha Chechik, Arie Gurfinkel
Comments (0)