Weakest precondition analysis for computer programs

摘要

Improved weakest condition analysis. In one embodiment, a computer-implemented method including first identifying a set of candidates of a computer program that are potentially defective, via a predetermined data flow analysis. In one embodiment, the predetermined data flow analysis may be a static single assignment analysis, or a partial redundancy analysis. Next, each of these candidates is examine via a weakest precondition analysis to determine whether the candidate actually is defective. The end result is a faster analysis, because the weakest precondition analysis is only performed on those candidates that are deemed potentially defective by the initial predetermined data flow analysis performed.