Modular and/or demand-driven string analysis of a computer program is performed. Each method of the program is encoded into monadic second-order logic (M2L) to yield a set of predicate declarations and a set of constraints. The two sets for each method are composed to yield a union set of predicate declarations and a union set of constraints for the program. The union set of constraints includes a particular set of constraints corresponding to call relationships among the methods. An M2L formula including a free variable corresponding to a program variable is added to the union set of constraints. The two union sets are processed to verify a satisfiability of the constraints in relation to an illegal pattern. Where the constraints are satisfiable, the program can generate a string containing the illegal pattern. Where the constraints are not satisfiable, the program never generates a string containing the illegal pattern.