Patent ID: 7930659

Claim:
A computer-implemented method for verifying a software program having a plurality of code statements, the method comprising the steps of: determining one or more properties of the software program to be verified; generating a model of the software program producing a predicate abstraction of the modeled software program; checking the abstracted model for correctness; generating an indication of the correctness; and refining the predicate abstraction by adding predicates, and checking the refined, abstracted model for correctness until no spurious counterexamples are produced; outputting an indication that the properties are satisfied or that the properties are disproved; wherein predicates are statement-specific localized to a basic block wherein a localized predicate exhibits a limited lifetime and never exists in all blocks of the program, wherein a basic block is represented by a single node of a control flow graph (CFG) and said predicates are determined using weakest pre-condition propagation along infeasible paths such that a plurality of calls made to any decision procedure when computing an abstraction of the software are eliminated.