Path feasibility analysis for string-manipulating programs

103Citations
Citations of this article
42Readers
Mendeley users who have this article in their library.

This article is free to access.

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 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. © 2009 Springer Berlin Heidelberg.

Cite

CITATION STYLE

APA

Bjørner, N., Tillmann, N., & Voronkov, A. (2009). Path feasibility analysis for string-manipulating programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5505 LNCS, pp. 307–321). https://doi.org/10.1007/978-3-642-00768-2_27

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free