Patent · US Active

Proof based bounded model checking

US8201116B2 · kind B2 · utility

0Cited by

2References

17Claims

0Family size

Assignee

International Business Machines Corporation · US

Inventors

Oded Fuhrmann · Jerusalem, IL
Alexander Ivrii · Haifa, IL
Tatyana Veksler · Jerusalem, IL

Key dates

Filing date	Aug 17, 2010
Grant date	Jun 12, 2012
Priority date	—
Expiry date	Dec 11, 2030

Classification

Technology area (CPC G)Physics
CPC primaryG06F30/3323
WIPO fieldComputer technology
WIPO sectorElectrical engineering

Abstract

An UNSAT core may be reused during iterations of a bounded model checking process. When increasing the bound, signals corresponding to signals within the UNSAT core may be used to represent the functionality of the model during cycles between the original bound and the increased bound. In case, consecutive unsatisfiability is determined in respect to different bounds, the same UNSAT core may be reused instead of computing a new UNSAT core.

Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.