Abstract Error Projection
Akash Lal, Nicholas Kidd, Thomas Reps, and Tayssir Touili
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 au- tomated 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.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)