Patent · US Active

Proof based bounded model checking

US8397192B2 · kind B2 · utility

1Cited by

4References

20Claims

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	Apr 15, 2012
Grant date	Mar 12, 2013
Priority date	—
Expiry date	Apr 15, 2032

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.