Patent ID: 8572574
Filing Date: 2013-10-29
Classification: G06F

Abstract:
1. A method comprising, by one or more computing devices: analyzing one or more first numeric constraints and one or more first string constraints associated with a software module, wherein: the software module comprises: one or more numeric variables; one or more string variables; one or more first operations that apply to specific ones of the numeric variables and produce numeric or string results; and one or more second operations that apply to specific ones of the string variables and produce numeric or string results; the first numeric constraints apply to specific ones of the numeric variables; and the first string constraints apply to specific ones of the string variables; inferring one or more second numeric constraints applying to specific ones of the string variables; inferring one or more second string constraints applying to specific ones of the numeric variables; representing each one of the first and second numeric constraints with an equation; representing each one of the first and second string constraints with a finite state machine; and validating the software module with respect to one or more requirements associated with the software module by attempting to solve for a solution comprising one or more values for specific ones of the numeric and string variables that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements, wherein attempting to solve for the solution that satisfies all the first and second numeric constraints, all the first and second string constraints, and all the requirements comprises: iteratively trying different possible values for the numeric and string variables and testing whether the possible values together produce a solution that satisfies all of the first and second numeric constraints, the first and second string constraints, and the requirements until a solution is found, the first and second numeric and string constraints are determined to be unsatisfiable, or a number of the iterations reaches a threshold; and if a solution is found, then outputting the values for the numeric and string variables.