Satisfiability (SAT) based bounded model checkers
US7835898B2 · kind B2 · utility
5Cited by
5References
2Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Nov 22, 2005 |
| Grant date | Nov 16, 2010 |
| Priority date | — |
| Expiry date | Jun 13, 2029 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method uses a SAT solver operating to cycle k to find bugs in a model having finite computation paths therein, wherein said bugs are on computation paths of less than length k. Another method includes adding an additional state variable to a model to be checked, where a governing state machine of the additional variable has a “sink” state. The method includes having a translation using the additional variable whenever a state indicates a bad state and performing satisfiability solving with the model and the translation.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.