Patent ID: 7058925

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 particular code statement in the program, and the particular code statement comprises a pointer and one of; a procedure call, an assignment, a goto statement, and a conditional statement; for each particular code statement in the program, generating one or more predicate statements that describe an effect of the particular code statement on the one or more predicates of interest; performing a pointer analysis to determine possible aliases of the pointer; computing the weakest precondition on the possible aliases of the pointer by computing the weakest precondition on a first case when the pointer has an alias and computing the weakest precondition on a second case when the pointer does not have an alias; and generating the boolean program in an abstractor based on the predicate statements.