Hiding irrelevant facts in verification conditions
AssigneeMicrosoft Corporation
InventorsK. 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.
Claims20
One or more computer-readable media including 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;
- determining dominators for the passive, acyclic intermediate language representation of the program;
- and
- generating a verification condition from the passive, acyclic intermediate language representation of the program, wherein the verification condition is structured according to the computed dominators such that when a theorem prover identifies a potential error, portions of the passive, acyclic intermediate language representation of the program irrelevant to the potential error are ignored.
A computer-implemented method for validating a program, comprising:
- translating a program to correspond to an intermediate language representation, wherein the intermediate language is expressible as a control-flow graph;
- generating a verification condition corresponding to the control-flow graph, wherein program blocks of the control-flow graph are represented by block equations in the verification condition;
- and
- structuring the verification condition such that when a potential error is encountered in association with the verification condition, remaining, unvalidated portions of the verification condition irrelevant to the potential error are ignored.
A program verification system, comprising:
- a program;
- a specification, wherein the program is validated against the specification;
- an intermediate language translator that is arranged to translate the program from its language to an intermediate language expressible by a control-flow graph;
- a loop eliminator that is arranged to eliminate the loops within the intermediate language representation of the program;
- a passive command module that is arranged to convert the intermediate language representation of the program to a passive intermediate language representation;
- a dominator determination module that is arranged to determine the dominator relationship between program blocks of the control-flow graph;
- a verification condition generator that is arranged to create a verification condition according to the dominator relationship and the passive intermediate language representation of the program;
- and
- a theorem prover, wherein the theorem prover ignores untested portions of the verification condition when a validated portion of the verification condition includes a potential error and the untested portions of the verification condition are irrelevant to the potential error.
Dependencies are inferred from the claim text.