System for verification using reachability overapproximation
US7475370B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Nov 12, 2007 |
| Grant date | Jan 6, 2009 |
| Priority date | — |
| Expiry date | Nov 12, 2027 |
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.