1. At a computer system, 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 is sufficiently precise to express the appropriate invariants; an act of associating 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 configured to 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.