Advertisement

Constraint Solving on Bounded String Variables

  • Joseph D. ScottEmail author
  • Pierre Flener
  • Justin Pearson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9075)

Abstract

Constraints on strings of unknown length occur in a wide variety of real-world problems, such as test case generation, program analysis, model checking, and web security. We describe a set of constraints sufficient to model many standard benchmark problems from these fields. For strings of an unknown length bounded by an integer, we describe propagators for these constraints. Finally, we provide an experimental comparison between a state-of-the-art dedicated string solver, CP approaches utilising fixed-length string solving, and our implementation extending an off-the-shelf CP solver.

Keywords

Constraint Programming Regular Language String Length Symbolic Execution String Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdulla, P.A., Atig, M.F., Chen, Y.-F., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150–166. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  2. 2.
    Allen, F.E.: Control flow analysis. ACM Sigplan Notices 5(7), 1–19 (1970)CrossRefGoogle Scholar
  3. 3.
    Barták, R.: Dynamic global constraints in backtracking based environments. Annals of Operations Research 118(1), 101–119 (2003)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Beldiceanu, N., Carlsson, M., Petit, T.: Deriving filtering algorithms from constraint checkers. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 107–122. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  5. 5.
    Bisht, P., Hinrichs, T., Skrupsky, N., Venkatakrishnan, V.N.: WAPTEC: whitebox analysis of web applications for parameter tampering exploit construction. In: Chen, Y., Danezis, G., Shmatikov, V. (eds.) Computer and Communications Security (CCS 2011), pp. 575–586. ACM (2011)Google Scholar
  6. 6.
    Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307–321. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  7. 7.
    Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering 2(3), 215–222 (1976)CrossRefGoogle Scholar
  8. 8.
    Emmi, M., Majumdar, R., Sen, K.: Dynamic test input generation for database applications. In: Rosenblum, D.S., Elbaum, S.G. (eds.) Software Testing and Analysis (ISSTA 2007), pp. 151–162. ACM (2007)Google Scholar
  9. 9.
    Fu, X., Powell, M.C., Bantegui, M., Li, C.C.: Simple linear string constraints. Formal Aspects of Computing 25, 847–891 (2013). sushi is available from http://people.hofstra.edu/Xiang_Fu/XiangFu/projects/SAFELI/SUSHI.php CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007). stp is available from https://sites.google.com/site/stpfastprover/ CrossRefGoogle Scholar
  11. 11.
    Gange, G., Navas, J.A., Stuckey, P.J., Søndergaard, H., Schachte, P.: Unbounded model-checking with interpolation for regular language constraints. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 277–291. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  12. 12.
    Gecode Team: Gecode: A generic constraint development environment (2006). http://www.gecode.org
  13. 13.
    Gervet, C.: Constraints over structured domains. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, chap. 17, pp. 605–638. Elsevier (2006)Google Scholar
  14. 14.
    Ghosh, I., Shafiei, N., Li, G., Chiang, W.F.: JST: an automatic test generation tool for industrial Java applications with strings. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) International Conference on Software Engineering (ICSE 2013), pp. 992–1001. IEEE / ACM (2013)Google Scholar
  15. 15.
    Golden, K., Pang, W.: Constraint reasoning over strings. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 377–391. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  16. 16.
    He, J., Flener, P., Pearson, J., Zhang, W.M.: Solving string constraints: the case for constraint programming. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 381–397. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  17. 17.
    Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Hind, M., Diwan, A. (eds.) Programming Language Design and Implementation (PLDI 2009), pp. 188–198. ACM (2009)Google Scholar
  18. 18.
    Hooimeijer, P., Weimer, W.: StrSolve: solving string constraints lazily. Automated Software Engineering 19(4), 531–559 (2012)CrossRefGoogle Scholar
  19. 19.
    Kieżun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: Rothermel, G., Dillon, L.K. (eds.) International Symposium on Software Testing and Analysis (ISSTA 2009), pp. 105–116. ACM (2009). hampi is available from http://people.csail.mit.edu/akiezun/hampi/
  20. 20.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)CrossRefzbMATHGoogle Scholar
  21. 21.
    Lothaire, M.: Combinatorics on words. Cambridge Mathematical Library, Cambridge University Press (1997)Google Scholar
  22. 22.
    Maher, M.J.: Open constraints in a boundable world. In: van Hoeve, W.-J., Hooker, J.N. (eds.) CPAIOR 2009. LNCS, vol. 5547, pp. 163–177. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  23. 23.
    Makanin, G.: The problem of solvability of equations in a free semigroup. Sbornik: Mathematics 32(2), 129–198 (1977)CrossRefzbMATHGoogle Scholar
  24. 24.
    Michel, L.D., Van Hentenryck, P.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 527–543. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  25. 25.
    Monette, J.-N., Flener, P., Pearson, J.: Towards solver-independent propagators. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 544–560. Springer, Heidelberg (2012). the indexical compiler is available from http://www.it.uu.se/research/group/astra/software#indexicals CrossRefGoogle Scholar
  26. 26.
    Pesant, G.: A regular language membership constraint for finite sequences of variables. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 482–495. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  27. 27.
    Quimper, C.-G., Walsh, T.: Global grammar constraints. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 751–755. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  28. 28.
    Redelinghuys, G., Visser, W., Geldenhuys, J.: Symbolic execution of programs with strings. In: Kroeze, J.H., de Villiers, R. (eds.) South African Institute of Computer Scientists and Information Technologists Conference (SAICSIT 2012), pp. 139–148. ACM (2012)Google Scholar
  29. 29.
    Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: Security and Privacy (S&P 2010), pp. 513–528. IEEE Computer Society (2010). kaluza is available from http://webblaze.cs.berkeley.edu/2010/kaluza/
  30. 30.
    Scott, J.D.: Rapid prototyping of a structured domain through indexical compilation. In: Schaus, P., Monette, J.N. (eds.) Domain Specific Languages in Combinatorial Optimization (CoSpeL workshop at CP 2013) (2013). http://cp2013.a4cp.org/workshops/cospel
  31. 31.
    Scott, J.D., Flener, P., Pearson, J.: Bounded strings for constraint programming. In: Tools with Artificial Intelligence (ICTAI 2013), pp. 1036–1043. IEEE Computer Society (2013)Google Scholar
  32. 32.
    Sellmann, M.: The theory of grammar constraints. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 530–544. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  33. 33.
    Trinh, M.T., Chu, D.H., Jaffar, J.: S3: A symbolic string solver for vulnerability detection in web applications. In: Computer and Communications Security (CCS 2014) (2014)Google Scholar
  34. 34.
    Van Hentenryck, P., Saraswat, V.A., Deville, Y.: Design, implementation, and evaluation of the constraint language cc(FD). techreport CS-93-02, Brown University, Providence, USA (January 1993), revised version: Journal of Logic Programming 37(1–3), 293–316 (1998)Google Scholar
  35. 35.
    Yu, F., Bultan, T., Ibarra, O.H.: Symbolic string verification: combining string analysis and size analysis. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 322–336. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  36. 36.
    Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: A Z3-based string solver for web application analysis. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Foundations of Software Engineering (FSE 2013), pp. 114–124. ACM (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Joseph D. Scott
    • 1
    Email author
  • Pierre Flener
    • 1
  • Justin Pearson
    • 1
  1. 1.Uppsala UniversityUppsalaSweden

Personalised recommendations