Satisfiability (SAT) based bounded model checkers
- 申请公布号：
- US8489380(B2)
- 申请号：
- US201113108008
- 申请日期：
- 2011.05.16
- 申请公布日期：
- 2013.07.16
- 申请人：
- GEIST DANIEL;GINZBURG MARK;LUSTIG YOAD;RABINOVOTZ ISHAI;SHACHAM OHAD;TZOREF RACHEL;INTERNATIONAL BUSINESS MACHINES CORPORATION
- 发明人：
- GEIST DANIEL;GINZBURG MARK;LUSTIG YOAD;RABINOVOTZ ISHAI;SHACHAM OHAD;TZOREF RACHEL
- 分类号：
- G06F17/50;G06F9/45
- 主分类号：
- G06F17/50
- 摘要：
- 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.
Copyright Notice © 2009-2024 传众 版权所有