Method for verification using reachability overapproximation
US7322017B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Dec 14, 2004 |
| Grant date | Jan 22, 2008 |
| Priority date | — |
| Expiry date | Dec 8, 2025 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method, system and computer program product for verifying that a design conforms to a desired property is disclosed. The method comprises receiving a design, a first initial state of the design, and a property for verification with respect to the design. The first initial state of the design is expanded to create a superset of the first initial state containing one or more states reachable from the first initial state of the design. A superset is synthesized to define a second initial state of the design. Application of the superset to the design is overapproximated through cutpoint insertion into the superset to obtain a modified superset, and the property is verified with reference to the modified superset.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.