发明名称 |
Satisfiability (SAT) based bounded model checkers |
摘要 |
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. |
申请公布号 |
US8108195(B2) |
申请公布日期 |
2012.01.31 |
申请号 |
US20100853318 |
申请日期 |
2010.08.10 |
申请人 |
GEIST DANIEL;GINZBURG MARK;LUSTIG YOAD;RABINOVITZ ISHAI;SHACHAM OHAD;TZOREF RACHEL;INTERNATIONAL BUSINESS MACHINES CORPORATION |
发明人 |
GEIST DANIEL;GINZBURG MARK;LUSTIG YOAD;RABINOVITZ ISHAI;SHACHAM OHAD;TZOREF RACHEL |
分类号 |
G06F17/50;G06F9/45 |
主分类号 |
G06F17/50 |
代理机构 |
|
代理人 |
|
主权项 |
|
地址 |
|