1. A computer readable medium having stored thereon computer executable instructions causing a computer to execute a process comprising: translating a program code to an logical representation that includes type-safety assertions; generating a verification condition from the translated program code; if the generated verification condition includes one or more universal quantifiers, removing the one or more universal quantifiers from the generated verification condition; and executing a decision procedure to prove or disprove the generated verification condition.