An object store model for diagnosing Java']Java programs

During the last decade many intelligent debugging tools have been developed to assist users to detect program errors in a software system. The tools based on formal verification reveal counterexamples in case a given program violates the specified properties. However, these counterexamples do not allow to locate the root cause sufficiently. In order to bridge the gap between counterexamples and root causes of failure we introduce a new model for localizing program errors. The model we use keeps track on object relations arising during program execution on the given counterexample. We have used the approach to isolate the errors in several small Java programs.