Efficient approaches for bounded model checking

A method for inductive proof of safety properties expressed in Linear Time Temporal Logic comprising:

• checking a k-instance base case on a negation of a given property, and checking a k-instance inductive step on a monitor predicate corresponding to the given property, starting from k=0 and increasing it up to a given specified limit,
• wherein the base case checking further comprises:
• translating the negated property into property checking schemas consisting of Boolean satisfiability checks, associated with temporal operators F(p), and X(p), wherein F represents an eventuality operator, and X represents a next-time operator;
• searching for a witness of the negated property, starting from the initial state, by repeated invocations of the property checking schemas for F(p), X(p) operators and standard handling of atomic propositions and Boolean operators;
• terminating the overall proof with success if it is proved that a witness cannot be found;
• terminating the overall proof with failure if a witness is found in k time frames;
• otherwise when it is inconclusive, continuing with the inductive step checking;
• wherein the inductive step checking consists of the following property checking schema:
• adding constraints to ensure that the monitor predicate holds for k time frames starting from an arbitrary state, and it does not hold in the k+1st time frame,
• if unsatisfiable, terminating the overall proof with success, otherwise, continuing the search;
• wherein the search is continued by increasing k up to the specified limit and repeating the base case and inductive step,
• wherein the proof is inconclusive if the specified limit for k is reached.

An inductive proof engine for circuits wherein the engine is capable of proving safety properties in Linear Time Logic temporal properties said engine comprising:

• a base case checker adapted to check a k-instance base case on a negation of a given property;
• an inductive step checker adapted to check a k-instance inductive step on a monitor predicate corresponding to the given property;
• a property translator adapted to translate negated properties into property checking schemas consisting of Boolean satisfiability checks, associated with temporal operators F(p) and X(p), wherein F represents an eventuality operator and X represents a next-time operator;
• and
• a searched adapted to search for a witness of the negated property.