Patent ID: 8402444
Filing Date: 2013-03-19
Classification: G06F

Abstract:
1. A method for validating a candidate trace produced by a Counter-Example Guided Abstraction Refinement (CEGAR) loop, the candidate trace associated with a potential error within a program, the method comprising: performing forward analysis in a forward direction along the candidate trace to collect information pertaining to the candidate trace, the information comprising values of variables stored during the forward analysis; performing backward analysis in a backward direction along the candidate trace on the basis of at least the values of the variables stored during the forward analysis, the forward analysis and the backward analysis identifying whether the candidate trace represents a feasible trace or an infeasible trace; and generating, for the case of the infeasible trace, at least one predicate for use in removing the infeasible trace from a subsequent iteration of the CEGAR loop in an instance when said at least one predicate can be discovered, wherein the method is performed by one or more processing devices.