Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Path Feasibility Analysis for String-Manipulating Programs

Nikolaj Bjørner, Nikolai Tillmann, and Andrei Voronkov


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 integer 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, report on the encouraging results and discuss directions for improving the method further.


Publication typeInproceedings
Published inProc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009
SeriesLecture Notes in Computer Science
PublisherSpringer Verlag

Previous versions

Nikolaj Bjorner, Nikolai Tillmann, and Andrei Voronkov. Path Feasibility Analysis for String-Manipulating Programs, Microsoft, October 2008.

> Publications > Path Feasibility Analysis for String-Manipulating Programs