Searching for counter-examples intelligently
AssigneeInternational Business Machines Corporation
InventorYoav Rodeh
Life of this patent
Estimating the term…
Abstract
A method for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states. The method includes assembling a first set of the states known to be reachable from the initial states in accordance with the transition relation, and defining a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation. The sets of the states are modified until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation. The counterexample is searched for over the states in the intersection.
Claims26
A method for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states, comprising:
- assembling a first set of the states known to be reachable from the initial states in accordance with the transition relation;
- defining a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation;
- modifying the sets of the states until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation;
- and
- searching for the counterexample over the states in the intersection.
A method for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states, comprising:
- assembling a first set of the states known to be reachable from the initial states in accordance with the transition relation;
- defining a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation;
- modifying the sets of the states until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation;
- and
- searching for the counterexample over the states in the intersection
- wherein modifying the sets of the states comprises iteratively modifying the first and second sets until the intersection is found, and
- wherein defining the second set of the states comprises defining n+1 sets of the states, referred to as D0 through Dn, wherein D0 comprises the bad states, such that for each value of an index i, which assumes values from 1 to n, it is estimated that one of the bad states can be reached in i steps of the transition relation from at least one of the states in Di, and wherein modifying the second set comprises:
- (a) choosing as candidates a subset of the states from the intersection of Di and the first set;
- (b) verifying that at least one of the candidates can reach one of the states in Di−1 in one step of the transition relation;
- (c) refining the estimate of Di when none of the candidates can reach in one step any of the states in Di−1;
- and
- (d) repeating steps (a) through (c) until one of the candidates is verified to reach one of the states in Di−1 in one step of the transition relation.
Apparatus for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states, the apparatus comprising a verification processor arranged to assemble a first set of the states known to be reachable from the initial states in accordance with the transition relation, to define a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation, to modify the sets of the states until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation, and to search for the counterexample over the states in the intersection.
Apparatus for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states, the apparatus comprising a verification processor arranged to assemble a first set of the states known to be reachable from the initial states in accordance with the transition relation, to define a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation, to modify the sets of the states until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation, and to search for the counterexample over the states in the intersection,
- wherein the processor is arranged to iteratively modify the first and second sets in accordance with the transition relation until the intersection is found, and
- wherein the verification processor defines the second set of states by defining n+1 sets of the states, referred to as D0 through Dn, wherein D0 comprises the bad states, such that for each value of an index i, which assumes values from 1 to n, the verification processor estimates that one of the bad states can be reached in i steps of the transition relation from at least one of the states in Di, and wherein the verification processor modifies the second set by choosing as candidates a subset of the states from the intersection of Di and the first set, by verifying that at least one of the candidates can reach one of the states in Di−1 in one step of the transition relation, by refining the estimate of Di when none of the candidates can reach in one step any of the states in Di−1, and by repeating such steps until one of the candidates is verified to reach one of the states in Di−1 in one step of the transition relation.
A computer software product for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states, the product comprising a computer-readable medium in which program instructions are stored, which instructions, when read by a computer, cause the computer to assemble a first set of the states known to be reachable from the initial states in accordance with the transition relation, to define a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation, to modify the sets of the states until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation, and to search for the counterexample over the states in the intersection.
Dependencies are inferred from the claim text.