Device, system and method for formal verification
US7725851B2 · kind B2 · utility
12Cited by
0References
15Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Aug 27, 2007 |
| Grant date | May 25, 2010 |
| Priority date | — |
| Expiry date | Jul 15, 2028 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Device, system and method of efficient automata-based implementation of liveness properties for formal verification. A system according to embodiments of the invention includes a property transformation module to receive an assume verification directive on a liveness property in a property specification language, and to translate the property a fairness statement that uses a deterministic automaton. The deterministic automaton is exponential in the size of the input property. The assume verification directive may be transformed into a strong suffix implication in the property specification language.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.