Computer implemented cover process approximating quantifier elimination
View Patent ↗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).
1. A symbolic model checking method of determining the reliability of a transition system described by the tuple (V, I(V), T(V old , V new ), E(V)), where V represents the set of state variables, I(V) is a formula describing the set of initial states, T(V old , V new ) is a formula describing the transition relation between the old values V old and new values V new of the variables in V, and E(V) is a formula describing the set of error states, wherein the formulas I(V) and T(V old , V new ) 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 CR 0 (V)≡I(V), and an i th state CR i (V)≡CR i−1 (V) ( V old : CR i−1 (V old ) T(V old , V)) for i>0,
where the expression ( V old : CR i−1 (V old ) T(V old , 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 i th state CR i (V) is an approximation of the i th state R i−1 (V) (∃V old : R i−1 (V old ) T(V old , V)) for i>0 if the formulas I(V) and T(V old , V new ) 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).
2. A method as recited in claim 1 , wherein the formulas I(V) and T(V old , V new ) contain one or more uninterpreted function symbols.
3. A method as recited in claim 1 , wherein the formulas I(V) and T(V old , V new ) contain symbols from a theory of lists.
4. A method as recited in claim 1 , wherein the formulas I(V) and T(V old , V new ) contain symbols from a theory of arrays.
5. A method as recited in claim 1 , further comprising a step (d) of determining all error states for the model.
6. A method as recited in claim 5 , further comprising a step (e) of determining whether there is an intersection between all reachable states determined in said steps (b) or (c) and the error states determined in said step (d).
7. A method as recited in claim 6 , wherein a determination in said step (e) of no intersection indicates a valid model.
8. A method as recited in claim 7 , wherein a determination in said step (e) of an intersection indicates errors in the model.
9. A method as recited in claim 8 , wherein an indication of validity is reliable and an indication of an error is reliable where said formula φ does not admit existential quantification.