Finding Feasible Abstract Counter-examples

A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the highcomputational cost of model checking most researchers advocate the use of aggressive property-preserving abstractions. Unfortunately, the more aggressively a system is abstracted the more infeasible behavior it will have. Thus, while abstraction enables efficient model checking it also threatens the usefulness of model checking as a defect detection tool, since it may be difficult to determine whether a counter-example is feasible and hence worth developer time to analyze. We have