Abstract Error Projection

摘要

In this paper, we extend model-checking technology with the notion of an error projection. Given a program abstraction, an error projection divides the program into two parts: the part outside the error projection is guaranteed to be correct, while the part inside the error projection can have bugs. Subsequent automated or manual verification effort need only be concentrated on the part inside the error projection. We present novel algorithms for computing error projections using weighted pushdown systems that are sound and complete for the class of Boolean programs and discuss additional applications for these algorithms.