Path feasibility analysis for string-manipulating programs. (English) Zbl 1234.68070
Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 307-321 (2009).
Summary: 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.
For the entire collection see [Zbl 1157.68007].
For the entire collection see [Zbl 1157.68007].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68W32 | Algorithms on strings |
References:
| [1] | Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005) · Zbl 1176.68116 · doi:10.1007/11609773_28 |
| [2] | Büchi, J.R., Senger, S.: Definability in the existential theory of concatenation. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik (1988) · Zbl 0635.03006 |
| [3] | Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: automatically generating inputs of death. In: CCS, pp. 322–335. ACM Press, New York (2006) |
| [4] | Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003) · Zbl 1067.68541 · doi:10.1007/3-540-44898-5_1 |
| [5] | Dong, Y., Quan, Q., Zhang, J.: Priority-based energy aware and coverage preserving routing for wireless sensor network. In: VTC Spring, pp. 138–142. IEEE, Los Alamitos (2008) |
| [6] | Fu, X., Lu, X., Peltsverger, B., Chen, S., Qian, K., Tao, L.: A Static Analysis Framework For Detecting SQL Injection Vulnerabilities. In: COMPSAC, pp. 87–96 (2007) · doi:10.1109/COMPSAC.2007.43 |
| [7] | Godefroid, P.: Compositional dynamic test generation. In: Proc. of POPL 2007, pp. 47–54. ACM Press, New York (2007) |
| [8] | Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. SIGPLAN Notices 40(6), 213–223 (2005) · doi:10.1145/1064978.1065036 |
| [9] | Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008) · Zbl 1139.03007 · doi:10.1007/978-3-540-78499-9_33 |
| [10] | Khoussainov, B., Nies, A., Rubin, S., Stephan, F.: Automatic structures: Richness and limitations. In: LICS, pp. 44–53 (2004) · Zbl 1128.03028 |
| [11] | King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976) · Zbl 0329.68018 · doi:10.1145/360248.360252 |
| [12] | Matiyasevich, Y.: Word Equations, Fibonacci Numbers, and Hilbert’s Tenth problem. In: Workshop on Fibonacci Words, vol. 43, pp. 36–39 (2007) |
| [13] | Ruan, H., Zhang, J., Yan, J.: Test Data Generation for C Programs with String-Handling Functions. Theoretical Aspects of Software Engineering 0, 219–226 (2008) |
| [14] | Sen, K., Agha, G.A.: CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419–423. Springer, Heidelberg (2006) · doi:10.1007/11817963_38 |
| [15] | Shannon, D., Hajra, S., Lee, A., Zhan, D., Khurshid, S.: Abstracting symbolic execution with string analysis. In: Taicpart-Mutation, Washington, DC, USA, pp. 13–22 (2007) · doi:10.1109/TAIC.PART.2007.34 |
| [16] | Tillmann, N., de Halleux, J.: Pex - white box test generation for .NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-79124-9_10 |
| [17] | Xie, T., Tillmann, N., de Halleux, P., Schulte, W.: Fitness-guided path exploration in dynamic symbolic execution. Technical Report MSR-TR-2008-123, Microsoft (2008) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
