Efficient approaches for bounded model checking
US7711525B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | May 30, 2002 |
| Grant date | May 4, 2010 |
| Priority date | — |
| Expiry date | May 5, 2026 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for bounded model checking of arbitrary Linear Time Logic temporal properties. The method comprises translating properties associated with temporal operators F(p), G(p), U(p, q) and X(p) into property checking schemas comprising Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator and X represents a next-time operator. The overall property is checked in a customized manner by repeated invocations of the property checking schemas for F(p), G(p), U(p, q), X(p) operators and standard handling of atomic propositions and Boolean operators.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.