Program verification and discovery using probabilistic inference
View Patent ↗In one embodiment, a computer system performs a method for verifying the validity or invalidity of a software routine by learning appropriate invariants at each program point. A computer system chooses an abstract domain that is sufficiently precise to express the appropriate invariants. The computer system associates an inconsistency measure with any two abstract elements of the abstract domain. The computer system searches for a set of local invariants configured to optimize a total inconsistency measure which includes a sum of local inconsistency measures. The computer system optimizes the total inconsistency measure for all input/output pairs of the software routine. In one embodiment, the optimization of total inconsistency is achieved by the computer system which repeatedly replaces a locally inconsistent invariant with a new invariant, randomly selected among the possible invariants which are locally less inconsistent with the current invariants at the neighboring program points.
1. At a computer system including a processor and system memory, a method for verifying the validity or invalidity of a software routine by learning appropriate invariants at each program point, the method comprising:
an act of choosing an abstract domain that expresses the appropriate invariants;
an act of associating, using the processor, a local inconsistency measure with any two abstract elements of the abstract domain, wherein the measure is a monotonic function of the difference of the sets of states represented by the two abstract elements of the abstract domain;
an act of searching for a set of local invariants that optimize a total inconsistency measure which includes a sum of local inconsistency measures;
an act of optimizing the total inconsistency measure for all input/output pairs of the software routine; and
an act of randomly selecting an invariant that is locally inconsistent with the invariant's neighboring invariants and replacing the selected invariant with an invariant that is less locally inconsistent.
2. The method of claim 1 , further comprising:
an act of determining whether an invariant at a program point is locally consistent with the invariant's neighboring invariants; and
upon determining that an invariant is locally inconsistent with the invariant's neighboring invariants, an act of sampling a different invariant that is less locally inconsistent with the invariant's neighboring invariants.
3. The method of claim 1 , wherein the abstract domain comprises a set of formulas with bounded Boolean connectives over difference constraints.
4. The method of claim 1 , wherein the inconsistency measure is the proportion of the disjuncts in the disjunctive normal form version of a first boolean formula that do not logically imply the conjuncts in the conjunctive normal form version of a second boolean formula.
5. The method of claim 1 , wherein the probability of selecting an invariant at a program point is inversely proportional to its local inconsistency.
6. The method of claim 1 , further comprising an act of repeating the acts of claim 1 until all invariants become locally consistent.
7. The method of claim 1 , wherein the number of possible abstract domains is unbounded.
8. The method of claim 1 , further comprising at least one of learning and discovering one or more small programs from the one or more program's specifications in terms of a set of the program's input-output behavior.
9. A computer program product comprising one or more computer readable storage media having stored thereon computer-executable instructions that, when executed by one or more processors of a computing system, cause the computing system to perform a method for verifying the validity or invalidity of a software routine by learning appropriate invariants at each program point, the method comprising:
an act of choosing an abstract domain that expresses the appropriate invariants;
an act of associating a local inconsistency measure with any two abstract elements of the abstract domain, wherein the measure is a monotonic function of the difference of the sets of states represented by the two abstract elements of the abstract domain;
an act of searching for a set of local invariants that optimize a total inconsistency measure which includes a sum of local inconsistency measures;
an act of optimizing the total inconsistency measure for all input/output pairs of the software routine; and
an act of randomly selecting an invariant that is locally inconsistent with the invariant's neighboring invariants and replacing the selected invariant with an invariant that is less locally inconsistent.
10. The computer program product of claim 9 , further comprising:
an act of determining whether an invariant at a program point is locally consistent with the invariant's neighboring invariants; and
upon determining that an invariant is locally inconsistent with the invariant's neighboring invariants, an act of sampling a different invariant that is less locally inconsistent with the invariant's neighboring invariants.
11. The computer program product of claim 9 , wherein the abstract domain comprises a set of formulas with bounded Boolean connectives over difference constraints.
12. The computer program product of claim 9 , wherein the inconsistency measure is the proportion of the disjuncts in the disjunctive normal form version of a first Boolean formula that do not logically imply the conjuncts in the conjunctive normal form version of a second Boolean formula.
13. The computer program product of claim 9 , wherein the probability of selecting an invariant at a program point is inversely proportional to its local inconsistency.
14. The computer program product of claim 9 , further comprising an act of repeating the acts of claim 9 until all invariants become locally consistent.
15. The computer program product of claim 9 , wherein the number of possible abstract domains is unbounded.
16. A computer system for verifying the validity or invalidity of a software routine by learning appropriate invariants at each program point, the system comprising:
a processor;
system memory;
an abstract domain selection module for choosing an abstract domain that expresses the appropriate invariants;
an inconsistency measure association module for associating an inconsistency measure with any two abstract elements of the abstract domain, wherein the measure is a monotonic function of the difference of the sets of states represented by the two abstract elements of the abstract domain
a local invariant searching module for searching for a set of local invariants that optimize a total inconsistency measure which includes a sum of local inconsistency measures;
an inconsistency measure optimization module for optimizing the total inconsistency measure for all input/output pairs of the software routine; and
an invariant selection module for randomly selecting an invariant that IS locally inconsistent with the invariant's neighboring invariants and replacing the selected invariant with an invariant that IS less locally inconsistent.
17. The system of claim 16 , the system further comprising:
a consistency determination module for determining whether an invariant at a program point is locally consistent with the invariant's neighboring invariants; and
an invariant sampling module that, upon determining that an invariant is locally inconsistent with the invariant's neighboring invariants, samples a different invariant that is less locally inconsistent with the invariant's neighboring invariants.
18. The system of claim 16 , wherein the abstract domain comprises a set of formulas with bounded boolean connectives over difference constraints.
19. The system of claim 16 , wherein the inconsistency measure is the proportion of the disjuncts in the disjunctive normal form version of a first boolean formula that do not logically imply the conjuncts in the conjunctive normal form version of a second boolean formula.
20. The system of claim 16 , wherein the probability of selecting an invariant at a program point is inversely proportional to its local inconsistency, and the method of claim 1 is repeated until all invariants become locally consistent.