Strings are a fundamental data type in programming languages. In fact, they are heavily used in programming languages like JavaScript, Python, and PHP, a fact that has led to subtle programming bugs and security vulnerabilities. For this reason, string analysis plays an increasingly more important role in the development of correct and secure software.

Fundamental works on string analysis began in the 2000s, starting from the work of Christensen et al., where grammars and regular languages were employed as abstractions. The late 2000s saw the rise of a new approach of constraint solving to string analysis (a.k.a. string solving) that has lasted up to this day. This began with several works including, where a new potential application to automated testing and detection of security vulnerabilities of web applications (e.g. cross-site scripting, written XSS for short) was outlined. Such a promising application has fueled much of the development of string solving in the following decade resulting in many novel results in both theory (decidability, complexity, expressivity) and implementations (dozens of string solvers, a standardized SMT-LIB string theory, as well as a string track at SMT-COMP). Today, strings represent the most used theory at Amazon Web Services, and string solvers at AWS are in particular used to analyze Role-Based Access Control (RBAC) policies.

Interestingly, the work of string constraints started more than half a century earlier with simple incomplete algorithms for equational constraints by Plotkin, which culminated in the 70s with the decidability result of Makanin. In the 2000s new approach, based on compression methods rather than string combinatorics, was discovered, resulting in much simpler arguments and smaller computational complexity. Although the field still has notoriously difficult open problems (e.g. decidability of string constraints with length constraints), some of these decidability results have been applied to the decision problem of non-structural subtype entailment in programming language theory.

In the last decade, theories, implementation, and applications of string solving have become a regular topic at POPL (e.g. in 2018, one full session was dedicated to it), and related conferences like PLDI and CAV. Despite this growing importance in the programming language community and the depth/breadth of the topic, string constraint solving has been commonly viewed as a complex and impenetrable topic. For this reason, we believe that a comprehensive tutorial on string solving — covering theory, implementations and applications under the same umbrella — would be beneficial and of interests to POPL audience.