Chain-free string constraints. (English) Zbl 1437.68131

Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 277-293 (2019).
Summary: We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable fragment of string constraints, called weakly chaining string constraints, for which we show that the satisfiability problem is decidable. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. We have developed a prototype implementation of our new decision procedure, and integrated it into in an existing framework that uses CEGAR with under-approximation of string constraints based on flattening. Our experimental results show the competitiveness and accuracy of the new framework.
For the entire collection see [Zbl 1428.68012].


68R07 Computational aspects of satisfiability
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI


[1] Abdulla, P.A., et al.: Trau String Solver. https://github.com/diepbp/FAT
[2] Abdulla, P.A., et al.: Flatten and conquer: a framework for efficient analysis of string constraints. In: PLDI. ACM (2017)
[3] Abdulla, P.A., et al.: Trau: SMT solver for string constraints. In: FMCAD. IEEE (2018)
[4] Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150-166. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_10
[5] Abdulla, P.A., et al.: Norn: an SMT solver for string constraints. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462-469. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_29
[6] Barceló, P., Figueira, D., Libkin, L.: Graph logics with rational relations. Logical Methods Comput. Sci. 9(3) (2013). https://doi.org/10.2168/LMCS-9(3:1)2013 · Zbl 1272.03147
[7] Berzish, M., Zheng, Y., Ganesh, V.: Z3str3: a string solver with theory-aware branching. CoRR abs/1704.07935 (2017)
[8] Büchi, J.R., Senger, S.: Definability in the existential theory of concatenation and undecidable extensions of this theory. Z. Math. Logik Grundlagen Math. 34(4) (1988) · Zbl 0635.03006
[9] Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the replace all function. Proc. ACM Program. Lang. 2(POPL) (2018). https://doi.org/10.1145/3158091
[10] Chen, T., Hague, M., Lin, A.W., Rümmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL) (2019). https://doi.org/10.1145/3290362
[11] de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
[12] Ganesh, V., Berzish, M.: Undecidability of a theory of strings, linear arithmetic over length, and string-number conversion. CoRR abs/1605.09442 (2016)
[13] Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what’s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209-226. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_21
[14] Holík, L., Janku, P., Lin, A.W., Rümmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. PACMPL 2(POPL) (2018). https://doi.org/10.1145/3158092
[15] Hu, Q., D’Antoni, L.: Automatic program inversion using symbolic transducers. In: SIGPLAN Notices, vol. 52, no. 6, June 2017
[16] Kausler, S., Sherman, E.: Evaluation of string constraint solvers in the context of symbolic execution. In: ASE 2014. ACM (2014)
[17] Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: ISTA 2009. ACM (2009)
[18] Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646-662. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_43
[19] Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: CVC4 (2016). http://cvc4.cs.nyu.edu/papers/CAV2014-strings/
[20] Lin, A.W., Barceló, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: POPL 2016. ACM (2016) · Zbl 1347.03060
[21] Makanin, G.: The problem of solvability of equations in a free semigroup. Math. USSR-Sbornik 32(2) (1977) · Zbl 0396.20037
[22] Matiyasevich, Y.: Computation paradigms in light of Hilbert’s tenth problem. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds.) New Computational Paradigms, pp. 59-85. Springer, New York (2008). https://doi.org/10.1007/978-0-387-68546-5_4 · Zbl 1136.03001
[23] Morvan, C.: On rational graphs. In: Tiuryn, J. (ed.) FoSSaCS 2000. LNCS, vol. 1784, pp. 252-266. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46432-8_17 · Zbl 0961.68107
[24] Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3) (2004) · Zbl 1192.68372
[25] Plandowski, W.: An efficient algorithm for solving word equations. In: STOC 2006. ACM (2006) · Zbl 1301.68165
[26] Quine, W.V.: Concatenation as a basis for arithmetic. J. Symb. Log. 11(4) (1946) · Zbl 0063.06362
[27] Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 453-474. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_24
[28] Robson, J.M., Diekert, V.: On quadratic word equations. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 217-226. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49116-3_20 · Zbl 0928.68088
[29] Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: IEEE Symposium on Security and Privacy. IEEE (2010)
[30] Saxena, P., Hanna, S., Poosankam, P., Song, D.: FLAX: systematic discovery of client-side validation vulnerabilities in rich web applications. In: NDSS. The Internet Society (2010)
[31] Schulz, K.U.: Makanin’s algorithm for word equations-two improvements and a generalization. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 85-150. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55124-7_4
[32] Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1136-1149. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27836-8_94 · Zbl 1099.03010
[33] Trinh, M.T., Chu, D.H., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: CCS 2014. ACM (2014)
[34] Trinh, M.-T., Chu, D.-H., Jaffar, J.: Progressive reasoning over recursively-defined strings. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 218-240. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_12 · Zbl 1411.68031
[35] TwistIt.tech: PHP tutorials (2019). https://www.makephpsites.com/php-tutorials/user-management-tools/changing-passwords.php. Accessed 29 Apr 2019
[36] Wang, H.-E., Tsai, T.-L., Lin, C.-H., Yu, F., Jiang, J.-H.R.: String analysis via automata manipulation with logic circuit representation. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 241-260. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_13 · Zbl 1411.68213
[37] Yu, F., Alkhalaf, M., Bultan, T.: Stranger: an automata-based string analysis tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 154-157. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_13
[38] Zheng, Y.
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.