Document Open Access Logo

Negated String Containment Is Decidable

Authors Vojtěch Havlena , Michal Hečko , Lukáš Holík , Ondřej Lengál

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.56.pdf
  • Filesize: 1.11 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
Keywords
  • not-contains
  • string constraints
  • word combinatorics
  • primitive word

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate ¬Contains(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.

Cite As Get BibTex

Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. Negated String Containment Is Decidable. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 56:1-56:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.56

Author Details

Vojtěch Havlena
  • Brno University of Technology, Czech Republic
Michal Hečko
  • Brno University of Technology, Czech Republic
Lukáš Holík
  • Aalborg University, Denmark
  • Brno University of Technology, Czech Republic
Ondřej Lengál
  • Brno University of Technology, Czech Republic

Funding

This work was supported by the Czech Ministry of Education, Youth and Sports ERC.CZ project LL1908, the Czech Science Foundation project 25-18318S, and the FIT BUT internal project FIT-S-23-8151. The work of Michal Hečko, a Brno Ph.D. Talent Scholarship Holder, is funded by the Brno City Municipality

Acknowledgements

We thank the anonymous reviewers for careful reading of the paper and their suggestions that greatly improved its quality.

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: A framework for efficient analysis of string constraints. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 602-617. ACM, 2017. URL: https://doi.org/10.1145/3062341.3062384.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer. Trau: SMT solver for string constraints. In Nikolaj S. Bjørner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pages 1-5. IEEE, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8602997.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Denghang Hu, Wei-Lun Tsai, Zhillin Wu, and Di-De Yen. Solving not-substring constraint with flat abstraction. In Programming Languages and Systems, pages 305-320, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-89051-3_17.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukáš Holík, and Petr Janků. Chain-free string constraints. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 277-293. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_16.
  5. C. Aiswarya, Soumodev Mal, and Prakash Saivasan. On the satisfiability of context-free string constraints with subword-ordering. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533329.
  6. Rajeev Alur and Pavol Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. SIGPLAN Not., 46(1):599-610, January 2011. URL: https://doi.org/10.1145/1925844.1926454.
  7. Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, and Nestan Tsiskaridze. Efficient solving of string constraints for security analysis. In William L. Scherlis and David Brumley, editors, Proceedings of the Symposium and Bootcamp on the Science of Security, Pittsburgh, PA, USA, April 19-21, 2016, pages 4-6. ACM, 2016. URL: https://doi.org/10.1145/2898375.2898393.
  8. Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka. Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci., 943:50-72, 2023. URL: https://doi.org/10.1016/j.tcs.2022.12.009.
  9. Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, and Vijay Ganesh. An SMT solver for regular expressions and linear arithmetic over string length. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 289-312. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_14.
  10. Berzish, Murphy. Z3str4: A solver for theories over strings. PhD thesis, University of Waterloo, 2021. URL: http://hdl.handle.net/10012/17102.
  11. Nikolaj S. Bjørner, Nikolai Tillmann, and Andrei Voronkov. Path feasibility analysis for string-manipulating programs. In Stefan Kowalewski and Anna Philippou, editors, 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, volume 5505 of Lecture Notes in Computer Science, pages 307-321. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00768-2_27.
  12. František Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Word equations in synergy with regular constraints. In Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker, editors, Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings, volume 14000 of Lecture Notes in Computer Science, pages 403-423. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-27481-7_23.
  13. Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. What is decidable about string constraints with the replaceall function. Proc. ACM Program. Lang., 2(POPL):3:1-3:29, 2018. URL: https://doi.org/10.1145/3158091.
  14. Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang., 6(POPL):1-31, 2022. URL: https://doi.org/10.1145/3498707.
  15. Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu. A decision procedure for path feasibility of string manipulating programs with integer data type. In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 325-342. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_18.
  16. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang., 3(POPL):49:1-49:30, 2019. URL: https://doi.org/10.1145/3290362.
  17. Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Solving string constraints with lengths by stabilization. Proceedings of the ACM on Programming Languages, 7(OOPSLA2):2112-2141, 2023. URL: https://doi.org/10.1145/3622872.
  18. Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Z3-Noodler: An automata-based string solver. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14570 of Lecture Notes in Computer Science, pages 24-33. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_2.
  19. Yu-Fang Chen, Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. A uniform framework for handling position constraints in string solving. Proc. ACM Program. Lang., 9(PLDI), 2025. URL: https://doi.org/10.1145/3729273.
  20. Joel D. Day, Thorsten Ehlers, Mitja Kulczynski, Florin Manea, Dirk Nowotka, and Danny Bøgsted Poulsen. On solving word equations using SAT. In RP'19, volume 11674 of LNCS, pages 93-106. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30806-3_8.
  21. Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea. On the expressive power of string constraints. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571203.
  22. Joel D. Day, Vijay Ganesh, Paul He, Florin Manea, and Dirk Nowotka. The satisfiability of extended word equations: The boundary between decidability and undecidability. CoRR, abs/1802.00523, 2018. URL: https://arxiv.org/abs/1802.00523.
  23. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  24. Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. Negated string containment is decidable (technical report). CoRR, abs/2506.22061, 2025. URL: https://arxiv.org/abs/2506.22061.
  25. Juhani Karhumäki, Filippo Mignosi, and Wojciech Plandowski. The expressibility of languages and relations by word equations. J. ACM, 47(3):483-505, 2000. URL: https://doi.org/10.1145/337244.337255.
  26. Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, and Morgan Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 646-662. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_43.
  27. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, and Morgan Deters. An efficient SMT solver for string constraints. Formal Methods Syst. Des., 48(3):206-234, 2016. URL: https://doi.org/10.1007/s10703-016-0247-6.
  28. Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark W. Barrett. A decision procedure for regular membership and length constraints over unbounded strings. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pages 135-150. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24246-0_9.
  29. Anthony Widjaja Lin and Pablo Barceló. String solving with word equations and transducers: Towards a logic for analysing mutation XSS. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 123-136. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837641.
  30. M. Lothaire, editor. Combinatorics on Words. Cambridge Mathematical Library. Cambridge University Press, 2 edition, 1997. Google Scholar
  31. M. Lothaire. Algebraic Combinatorics on Words. Cambridge University Press, 2002. Google Scholar
  32. Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, and Dirk Nowotka. Solving string constraints using sat. In Constantin Enea and Akash Lal, editors, Computer Aided Verification, pages 187-208, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-37703-7_9.
  33. Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel D. Day, Florin Manea, and Vijay Ganesh. Layered and staged Monte Carlo tree search for SMT strategy synthesis. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, pages 1907-1915. ijcai.org, 2024. URL: https://www.ijcai.org/proceedings/2024/211.
  34. R. C. Lyndon and M. P. Schützenberger. The equation a^M = b^Nc^P in a free group. Michigan Mathematical Journal, 9(4):289-298, 1962. URL: https://doi.org/10.1307/mmj/1028998766.
  35. G S Makanin. The problem of solvability of equations in a free semigroup. Mathematics of the USSR-Sbornik, 32(2):129, February 1977. URL: https://doi.org/10.1070/SM1977v032n02ABEH002376.
  36. Jakob Nielsen. Die isomorphismen der allgemeinen, unendlichen gruppe mit zwei erzeugenden. Mathematische Annalen, 78(1):385-397, 1917. Google Scholar
  37. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. Syntax-guided quantifier instantiation. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 145-163. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_8.
  38. Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, and Cesare Tinelli. Even faster conflicts and lazier reductions for string solvers. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 205-226. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_11.
  39. Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. In 40th Annual Symposium on Foundations of Computer Science, FOCS '99, 17-18 October, 1999, New York, NY, USA, pages 495-500. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814622.
  40. Andrew Reynolds, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. High-level abstractions for simplifying extended string constraints in SMT. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, volume 11562 of Lecture Notes in Computer Science, pages 23-42. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_2.
  41. Andrew Reynolds, Andres Nötzli, Clark W. Barrett, and Cesare Tinelli. Reductions for strings and regular expressions revisited. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 225-235. IEEE, 2020. URL: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_30.
  42. Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli. Scaling up DPLL(T) string solvers using context-dependent simplification. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 453-474. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_24.
  43. Neha Rungta. A billion SMT queries a day (invited paper). In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 3-18. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_1.
  44. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. A symbolic execution framework for JavaScript. In 31st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland, California, USA, pages 513-528. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/SP.2010.38.
  45. Trauc string constraints benchmark collection, 2020. URL: https://github.com/plfm-iis/trauc_benchmarks.
  46. Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, and Sergey Bereg. Monadic decomposition. J. ACM, 64(2):14:1-14:28, 2017. URL: https://doi.org/10.1145/3040488.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact