LNCS 5505 - Path strongFeasibilitystrong Analysis for String-Manipulating.pdfVIP

Path Feasibility Analysis for String-Manipulating Programs 1 1 2 Nikolaj Bjørner , Nikolai Tillmann , and Andrei Voronkov 1 Microsoft Research 2 University of Manchester Abstract. We discuss the problem of path feasibility for programs manipulating strings using a collection of standard string library functions. We prove results on the complexity of this problem, including its undecidability in the general case and decidability of some special cases. In the context of test-case generation, we are interested in an efficient finite model finding method for string constraints. To this end we develop a two-tier finite model finding procedure. First, an inte- ger abstraction of string constraints are passed to an SMT (Satisfiability Modulo Theories) solver. The abstraction is either unsatisfiable, or the solver produces a model that fixes lengths of enough strings to reduce the entire problem to be finite domain. The resulting fixed-length string constraints are then solved in a second phase. We implemented the procedure in a symbolic execution framework, re- port on the encouraging results and discuss directions for improving the method further. 1 Introduction Dynamic symbolic execution [8,3,14,16] has recently gained attention in the context of test-case generation. It extends static symbolic execution [11] by collecting sym- bolic constraints from concrete execution traces obtained by monitoring the executed instructions. In order to explore a different execution path it suffices to modify one of the extracted symbolic traces by selecting and