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.
This tutorial at POPL'24 aims at presenting a comprehensive, accessible and hands-on overview of the state-of-the-art of string solving for verification. This includes theoretical underpinnings, implementation techniques, and applications (specifically, to program analysis). It also includes hands-on experimentation with the string solver OSTRICH developed by us.
OSTRICH is an SMT solver for string constraints. Constraints for OSTRICH can be written using a superset of a subset of the SMT-LIB string theory. For more details, see the OSTRICH github page.