Patent · US Active

Utilizing an unSAT proof for model checking

US8161433B2 · kind B2 · utility

0Cited by

2References

25Claims

0Family size

Assignee

International Business Machines Corporation · US

Inventors

Oded Fuhrmann · Jerusalem, IL
Shlomo Hoory · Kfar Kara, IL
Ohad Shacham · Kfar Monash, IL

Key dates

Filing date	Jul 13, 2009
Grant date	Apr 17, 2012
Priority date	—
Expiry date	Jun 23, 2030

Classification

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

Abstract

A proof of unsatisfiability associated with a bounded model may be extended to apply to another bounded model having a larger bound. In some exemplary embodiments, an unbounded model may be proved using one or more such extensions. A proof may be reordered in order to decrease its size and increase the productivity of systems that utilize it. The proof may be reorder by a natural temporal order of cycles.

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