Back to results
US 7,926,037 B2Granted
Hiding irrelevant facts in verification conditions
AssigneeMicrosoft Corporation
InventorsK. Rustan M. Leino, Michael Barnett
Life of this patent
Estimating the term…
Abstract
A program verification process begins by converting a language of the program from a first language into an intermediate language representation. The loops of the program are eliminated. The program is converted from the intermediate language representation into a passive form. Dominators for the passive form of the program are determined. A verification condition is generated from the passive form of the program. The verification condition is structured according to the computed dominators such that when a theorem prover identifies a potential error, portions of the passive form of the program irrelevant to the potential error are ignored.
Claims13
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.
7 more elements
A computer-implemented method for validating a program, comprising:
- translating a program to correspond to an intermediate language representation, wherein the intermediate language is expressed as a control-flow graph comprising a plurality of program blocks each corresponding to a specific section of the program;
- and
- generating a verification condition corresponding to the control-flow graph, 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 of a plurality of dominating program blocks,
- wherein the hierarchically structured block equations of the verification condition causes a theorem prover to:
- 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.
5 more elements
A program verification system, comprising:
- a processor implementing instructions encoded on a non-transitory medium thereon to verify a program;
- a specification, wherein the program is validated against the specification;
- an intermediate language translator that is executed by a processor to translate the program from its language to an intermediate language expressible by a control-flow graph;
- a loop eliminator that is executed by a processor to eliminate the loops within the intermediate language representation of the program;
- a passive command module that is executed by a processor to convert the intermediate language representation of the program to a passive intermediate language representation, 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;
- a dominator determination module that is executed by a processor to determine the dominator relationship between program blocks of the control-flow graph;
- a verification condition generator that is executed by a processor to create a verification condition according to the dominator relationship and the passive intermediate language representation of the program, wherein the verification condition includes 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 dominator relationship;
- and
- a theorem prover, wherein the theorem prover:
- receives the verification condition,
- evaluates a first level of the hierarchically structured block equations prior to evaluating a subordinate level of hierarchical structured block equations,
- evaluates 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.
11 more elements
Dependencies are inferred from the claim text.