Patent ID: 8381199

Claim:
A method for performing modular string analysis of a computer program, comprising: dividing the computer program into a plurality of methods, by a processor; for each method of the computer program, encoding the method into monadic second-order logic (M2L) by the processor to yield a set of predicate declarations and a set of constraints for the method; composing the sets of predicate declarations and the sets of constraints for the methods of the computer program by the processor to yield a union set of predicate declarations and a union set of constraints for the computer program, the union set of constraints including a particular set of constraints corresponding to call relationships among the methods of the computer program; adding an M2L formula to the union set of constraints, by the processor, the M2L formula including a free variable corresponding to a program variable of the computer program; processing the constraints within the union set of constraints and the predicate declarations within the union set of predicate declarations by the processor using an M2L solver program to verify a satisfiability of the constraints in relation to an illegal pattern represented by an M2L predicate; where the constraints are satisfiable, reporting by the processor that the computer program can generate a string containing the illegal pattern; and, where the constraints are not satisfiable, reporting by the processor that the computer program never generates a string containing the illegal pattern.