Patent ID: 7729999

Claim:
At a computer system including a processor and system memory, a method for verifying the validity or invalidity of a software routine by learning appropriate invariants at each program point, the method comprising: an act of choosing an abstract domain that expresses the appropriate invariants; an act of associating, using the processor, a local inconsistency measure with any two abstract elements of the abstract domain, wherein the measure is a monotonic function of the difference of the sets of states represented by the two abstract elements of the abstract domain; an act of searching for a set of local invariants that optimize a total inconsistency measure which includes a sum of local inconsistency measures; an act of optimizing the total inconsistency measure for all input/output pairs of the software routine; and an act of randomly selecting an invariant that is locally inconsistent with the invariant's neighboring invariants and replacing the selected invariant with an invariant that is less locally inconsistent.