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 received input for predicate abstraction.