Patent ID: 7926037

Claim:
A computer-readable storage having computer-executable instructions for verifying a program, comprising: converting a programming language of the program into an intermediate language; eliminating loops within the program represented by the intermediate language such that the program corresponds to an acyclic intermediate language representation of the program; converting the program from the acyclic intermediate language representation into a passive, acyclic intermediate language representation comprising a plurality of program blocks each corresponding to a specific section of the program; determining dominators for the passive, acyclic intermediate language representation of the program, wherein the passive command module converts the intermediate language representation of the program to a passive intermediate language program by replacing assignment statements in the intermediate language representation with assume statements; and generating a verification condition from the passive, acyclic intermediate language representation of the program, the verification condition comprising a plurality of hierarchically structured block equations each assigned to one of the plurality of program blocks, wherein each block equation comprises a first term associated with an assigned program block and a term associated with each dominating program block according to the determined dominators, wherein the plurality of hierarchically structured block equations of the verification condition causes a theorem prover to: randomly evaluate a first level of the hierarchically structured block equations prior to evaluating a subordinate level of hierarchical structured block equations, evaluate the subordinate level of hierarchical structured block equations when the first level of hierarchically structured block equations is valid; and ignore the subordinate level of hierarchically structured block equations when the first level of hierarchically structure block equations is not valid.