Computer implemented cover process approximating quantifier elimination
AssigneeMicrosoft Corporation
InventorsMadanlal S. Musuvathi, Sumit Gulwani
Life of this patent
Estimating the term…
Abstract
A computer implemented cover process is disclosed for use in program analysis and verification techniques where existential quantifier elimination is not possible. The cover process allows an accurate assessment of the viability of a theory. Where a theory can be described using quantifier-free formulas, it can be shown that the program analysis and verification techniques using cover are not only sound (i.e., an indication of validity is reliable), but also precise (i.e., and indication of an error is reliable).
Claims9
A symbolic model checking method of determining the reliability of a transition system described by the tuple (V, I(V), T(Vold, Vnew), E(V)), where V represents the set of state variables, I(V) is a formula describing the set of initial states, T(Vold, Vnew) is a formula describing the transition relation between the old values Vold and new values Vnew of the variables in V, and E(V) is a formula describing the set of error states, wherein the formulas I(V) and T(Vold, Vnew) do not admit existential quantification, the method comprising the steps of:
- a. computing the set of reachable states CR(V) iteratively from an initial state CR0(V)≡I(V), and an ith state CRi(V)≡CRi−1(V) (Vold:
- CRi−1(Vold) T(Vold, V)) for i>0,
- where the expression (Vold:
- CRi−1(Vold) T(Vold, V)) represents a set of steps that can be reached in one step from the set of steps that can be reached in i−1 steps, and
- where the ith state CRi(V) is an approximation of the ith state Ri−1(V) (∃Vold:
- Ri−1(Vold) T(Vold, V)) for i>0 if the formulas I(V) and T(Vold, Vnew) admitted existential quantifier elimination;
- b. determining all sets of error states E(V);
- c. determining the reliability of the transition system by whether there is an intersection between the reachable states determined in said step (a) and the error states determined in said step (b);
- and
- d. reporting the reliability determined in said step (c).
Dependencies are inferred from the claim text.