Satisfiability (SAT) based bounded model checkers
US8489380B2 · kind B2 · utility
0Cited by
5References
20Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | May 16, 2011 |
| Grant date | Jul 16, 2013 |
| Priority date | — |
| Expiry date | Nov 15, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Systems and methods that use a solver to find bugs in a target model of a computing system having one or more finite computation paths are provided. The bugs on computation paths of less than a predetermined length are detected by translating the target model to include a state variable AF for one or more states of the target model, wherein AF(S) represents value of the state variable AF at state S; and solving the translated version of the target model that satisfies predetermined constrains.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.