Invention Grant
- Patent Title: Satisfiability (SAT) based bounded model checkers
- Patent Title (中): 满意度（SAT）的有界模型检查器
-
Application No.: US13108008Application Date: 2011-05-16
-
Publication No.: US08489380B2Publication Date: 2013-07-16
- Inventor: Daniel Geist , Mark Ginzburg , Yoad Lustig , Ishai Rabinovotz , Ohad Shacham , Rachel Tzoref
- Applicant: Daniel Geist , Mark Ginzburg , Yoad Lustig , Ishai Rabinovotz , Ohad Shacham , Rachel Tzoref
- Applicant Address: US NY Armonk
- Assignee: International Business Machines Corporation
- Current Assignee: International Business Machines Corporation
- Current Assignee Address: US NY Armonk
- Main IPC: G06F17/50
- IPC: G06F17/50 ; G06F9/45
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.
Public/Granted literature
- US20110213605A1 Satisfiability (SAT) Based Bounded Model Checkers Public/Granted day:2011-09-01
Information query
