Patent Document ID: 7587707
Application ID: 11172760

Base Claim:
1. A method of performing predicate abstraction for a computer program, the method comprising: receiving input for predicate abstraction of the computer program; and using a symbolic decision procedure, generating a predicate abstraction for the computer program based on the input for predicate abstraction; wherein the input for predicate abstraction comprises a set of predicates representing observations of expected behavior of the computer program, and a formula of interest; and wherein the symbolic decision procedure comprises a first saturation decision procedure having a first inference rule directed to a first type of logic used to derive a first set of derived predicates, the first saturation decision procedure comprising: repeatedly applying the first inference rule to predicates within the set of predicates to derive new predicates; and adding the new predicates to the set of predicates; such that repeatedly applying the first inference rule to the predicates in the set of predicates is stopped when applying the first inference rule derives no new predicates; wherein the first saturation decision procedure further comprises: determining if the formula of interest is present in the first set of derived predicates; determining that if the formula of interest occurs in the set of predicates then the formula of interest is consistent with the first set of derived predicates; and determining that if the formula of interest is not in the first set of derived predicates, then the formula of interest is inconsistent with the first inference rule.

---

Claim 2:
2. The method of claim 1 wherein the set of inference rules comprises at least one inference rule for deriving contradiction.