Patent ID: 7657867

Claim:
A computer-implemented method for generating a boolean program that is a predicate abstraction of a program having a plurality of code statements, the method comprising: receiving a plurality of predicates that define properties for the program; for each code statement in the program, identifying one or more predicates of interest out of the plurality of predicates, wherein the predicates of interest are affected by a procedure call in the program; for each particular procedure call in the program, generating one or more predicate statements that describe an effect of the particular procedure call on the one or more predicates of interest, wherein generating the one or more predicate statements that describe the effect of the procedure call includes: translating each formal parameter of a called boolean procedure into a calling context associated with a calling boolean procedure, assigning each return value of the called boolean procedure to a new variable in the calling boolean procedure, translating return predicates of the called boolean procedure into the calling context, and updating the predicates of interest; and generating the boolean program based on the predicate statements.