US Patent 7711525 Efficient approaches for bounded model checking

Patent 7711525 was granted and assigned to NEC Corporation on May, 2010 by the United States Patent and Trademark Office.

Overview Structured Data Issues Contributors Activity

Is a

Patent

Patent attributes

Current Assignee

Patent Jurisdiction

United States Patent and Trademark Office

Patent Number

77115250

Patent Inventor Names

Zijiang Yang0

Lintao Zhang0

Malay Ganai0

Pranav Ashar0

Aarti Gupta0

Date of Patent

May 4, 2010

Patent Application Number

101574860

Date Filed

May 30, 2002

Patent Primary Examiner

‌

Jason Proctor

Patent abstract

A method for bounded model checking of arbitrary Linear Time Logic temporal properties. The method comprises translating properties associated with temporal operators F(p), G(p), U(p, q) and X(p) into property checking schemas comprising Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator and X represents a next-time operator. The overall property is checked in a customized manner by repeated invocations of the property checking schemas for F(p), G(p), U(p, q), X(p) operators and standard handling of atomic propositions and Boolean operators.