MIXED NUMERIC AND STRING CONSTRAINT ANALYSIS

A method of determining whether a set of constraints is satisfiable may include identifying a set of constraints associated with a software module. The method may also include modeling a string associated with a string constraint of the set of constraints as a parameterized array. Further, the method may include determining the satisfiability of the set of constraints based on a representation of the string constraint as a quantified expression. The satisfiability of the set of constraints may also be based on elimination of a quantifier associated with the quantified expression such that the string constraint is represented as a numeric constraint. The representation of the string constraint as a quantified expression may be based on the parameterized array that is associated with the string.