SpringerLink
Log in

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

  • Conference paper
  • First Online:
Frontiers of Combining Systems (FroCoS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9322))

Included in the following conference series:

Abstract

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux calculus for that fragment which uses as oracles a decision procedure for linear integer arithmetic and a number of computable functions over regular expressions. A distinguishing feature of this calculus is that it provides a completely algebraic method for solving membership constraints which can be easily integrated into multi-theory SMT solvers. Another is that it can be used to generate symbolic solutions for such constraints, that is, solved forms that provide simple and compact representations of entire sets of complete solutions. The calculus is part of a larger one providing the theoretical foundations of a high performance theory solver for string constraints implemented in the SMT solver CVC4.

This work was partially funded by NSF grants #1228765 and #1228768.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  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)

    Google Scholar 

  2. Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  3. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

    Google Scholar 

  4. Badban, B., Dashti, M.: Semi-linear parikh images of regular expressions via reduction. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 653–664. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, chapter 26, pp. 825–885. IOS Press, February 2008

    Google Scholar 

  6. Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theor. Comput. Sci. 48(1), 117–126 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. Fu, X., Chih Li, C.: A string constraint solver for detecting web application vulnerability. In: Proceedings of the 22nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2010. Knowledge Systems Institute Graduate (2010)

    Google Scholar 

  10. Ghosh, I., Shafiei, N., Li, G., Chiang, W.-F.: JST: An automatic test generation tool for industrial Java applications with strings. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013, pp. 992–1001. IEEE Press, Piscataway (2013)

    Google Scholar 

  11. Henriksen, J.G., Jensen, J.L., Jørgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  12. Hooimeijer, P., Veanes, M.: An evaluation of automata algorithms for string analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 248–262. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 188–198. ACM (2009)

    Google Scholar 

  14. Hooimeijer, P., Weimer, W.: Solving string constraints lazily. In: Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, pp. 377–386. ACM (2010)

    Google Scholar 

  15. Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, pp. 105–116. ACM (2009)

    Google Scholar 

  16. Klarlund, N., Møller, A.: MONA implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 182–194. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Kozen, D.: Lower bounds for natural proof systems. In: FOCS, pp. 254–266. IEEE Computer Society (1977)

    Google Scholar 

  18. Li, G., Ghosh, I.: PASS: String solving with parameterized array and interval automaton. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 15–31. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  19. 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, Heidelberg (2014)

    Google Scholar 

  20. Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. Technical report, Department of Computer Science, The University of Iowa (2015). http://www.cs.uiowa.edu/~tinelli/papers.html

  21. Lu, K.Z.M.: XHaskell - Adding Regular Expression Type to Haskell. PhD thesis, National University of Singapore (2009)

    Google Scholar 

  22. Makanin, G.S.: The problem of solvability of equations in a free semigroup. English Rransl. in Math USSR Sbornik 32, 147–236 (1977)

    MathSciNet  MATH  Google Scholar 

  23. Matiyasevich, Y.V.: Hilbert’s tenth problem and paradigms of computation. In: Cooper, S.B., Löwe, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol. 3526, pp. 310–321. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. Parikh, R.J.: On context-free languages. J. ACM 13(4), 570–581 (1966)

    Article  MathSciNet  MATH  Google Scholar 

  25. Plandowski, W.: Satisfiability of word equations with constants is in pspace. J. ACM 51(3), 483–496 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  26. Rosu, G., Viswanathan, M.: Testing extended regular language membership incrementally by rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 499–514. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  27. Schulz, K. (ed.): Word Equations and Related Topics. Springer-Verlag New York, Inc., New York (1990)

    Google Scholar 

  28. Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. ACM Trans. Softw. Eng. Methodol. 33, 1–33 (2013)

    Article  Google Scholar 

  29. 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)

    Chapter  Google Scholar 

  30. Trinh, M.-T., Chu, D.-H., Jaffar, J.: S3: A symbolic string solver for vulnerability detection in web applications. In: Yung, M., Li, N. (eds.) Proceedings of the 21st ACM Conference on Computer and Communications Security (2014)

    Google Scholar 

  31. Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16–23. Springer, Heidelberg (2013)

    Google Scholar 

  32. Veanes, M., Bjørner, N., de Moura, L.: Symbolic automata constraint solving. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 640–654. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  33. 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)

    Chapter  Google Scholar 

  34. Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: A z3-based string solver for web application analysis. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pp. 114–124. ACM, New York (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Iowa, Iowa, USA

    Tianyi Liang, Nestan Tsiskaridze & Cesare Tinelli

  2. École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland

    Andrew Reynolds

  3. Department of Computer Science, New York University, New York, USA

    Clark Barrett

Authors
  1. Tianyi Liang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nestan Tsiskaridze
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrew Reynolds
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Cesare Tinelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Clark Barrett
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Universität Bremen, Bremen, Germany

    Carsten Lutz

  2. Fondazione Bruno Kessler, Trento, Italy

    Silvio Ranise

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C. (2015). A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. In: Lutz, C., Ranise, S. (eds) Frontiers of Combining Systems. FroCoS 2015. Lecture Notes in Computer Science(), vol 9322. Springer, Cham. https://doi.org/10.1007/978-3-319-24246-0_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24246-0_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24245-3

  • Online ISBN: 978-3-319-24246-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation