To improve the reporting of results from model checking and program-analysis systems, we introduce the notion of an error projection and annotated error projection. An error projection is a set of program nodes N such that for each node n in N there exists an (abstract) error path from the program entry s through n to a specified target node t. An annotated error projection associates with each node n in the error projection an (abstract) counterexample that validates the error along with an abstract store, whose presence at n induces the error. We present novel algorithms for computing (annotated) error projections and discuss additional applications for these algorithms. Our experiments show that error projections can be computed efficiently.

(Click here to access the paper: PDF)