System and method for verifying computer program correctness and providing recoverable execution trace information

A computer program product for use in static checking in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:

• a verification condition generator that converts a specified program into a logical equation representing the predefined set of conditions as applied to instructions and elements of the instructions of the program, the verification condition generator including instructions that insert flow control labels into the sub-equations of the logical equation, the flow control labels identifying conditional branch points in the specified computer program;
• a theorem prover that processes the logical equation to determine the truth of the logical equation, and when the truth of the logical equation cannot be proved, generates at least one counter-example identifying one of the conditions, one or more variable values inconsistent with the one condition, and any of the flow control labels for conditional branch points of the program associated with the identified variable values;
• and
• a post processing module that converts the at least one counter-example into an error message that includes a program trace that identifies a path through the computer program when the counter-example identifies one or more of the flow control labels.

A method, comprising:

• converting a computer program into a logical equation representing a predefined set of conditions;
• inserting flow control labels into sub-equations of the logical equation, the flow control labels identifying branch points in the computer program, wherein at least one of the flow control labels is of a form selected from the group consisting of (1) L==>P wherein L is a flow control label name and P is a subcomponent of the logical equation, (2) L=K==>P wherein L is a flow control label name, k is a constant value and P is a subcomponent of the logical equation, (3) {LBLPOS L P} wherein L is a flow control label name and P is a subcomponent of the logical equation, (4) {LBLNEG L P} wherein L is a flow control label name and P is a subcomponent of the logical equation, and (5) {LBLPOS L True}==>P wherein L is a flow control label name and P is a subcomponent of the logical equation;
• applying a theorem prover to the logical equation to determine a truth of the logical equation, and when the truth of the logical equation cannot be proved, generating at least one counter-example identifying one of the conditions;
• and
• converting the at least one counter-example into an error message that comprises a program trace that identifies a path through the computer program when the counter-example identifies one or more of the flow control labels.