Patent Number: 7,711,525

Title: Efficient approaches for bounded model checking

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.

Inventors: Ganai; Malay (Plainsboro, NJ), Zhang; Lintao (Princeton, NJ), Gupta; Aarti (Princeton, NJ), Yang; Zijiang (Plainsboro, NJ), Ashar; Pranav (Belle Mead, NJ)

Assignee: NEC Corporation

International Classification: G06F 17/10 (20060101)

Expiration Date: 5/04/12018