Patent ID: 7287243

Claim:
A code verification system, comprising: memory for storing a compiled program; and logic configured to translate the compiled program into a set of human-readable instructions and construct a coarse tree representing a program flow of the set of human-readable instructions, the logic configured to compute, based on the coarse tree, type signatures representative of code constructs of the compiled program, each of the type signatures specifying a respective type constraint for the code constructs, the type signatures including a first type signature representative of at least one instruction in a first path in the program flow and a second type signature representative of at least one instruction in a second path that is alternative to the first path in the program flow, the logic further configured to compute a merged signature by merging the first and second type signatures, wherein the merged signature has a partial output binding indicating that the at least one instruction in the first path leaves a variable undisturbed and the at least one instruction in the second path writes, to the variable, a data type specified by the partial output binding, and to compose the merged signature with a third type signature to form a composed signature, the logic further configured to perform type checking for the compiled program based on the composed signature and to indicate whether the compiled program passed the type checking.