Searching for counter-examples intelligently
US6587998B2 · kind B2 · utility
Assignee
Inventor
Key dates
| Filing date | Jan 16, 2001 |
| Grant date | Jul 1, 2003 |
| Priority date | — |
| Expiry date | Jul 29, 2021 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.