1. 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, the predicates of interest being affected by a particular code statement in the program, the particular code statement including one of a procedure call, an assignment, a goto statement, and a conditional statement; and 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, the predicate statements thus forming the boolean program.