String Solving for Verification - TutorialFest at POPL 2024

Explore the world of string solving for verification in this comprehensive 3.5-hour tutorial from ACM SIGPLAN's TutorialFest at POPL'24. Delve into the fundamental role of strings in programming languages and their impact on software correctness and security. Trace the evolution of string analysis from its roots in the 2000s to the modern constraint solving approach. Discover how string solving has become crucial in detecting security vulnerabilities, particularly in web applications. Learn about the theoretical foundations, including decidability results and complexity analysis, as well as practical implementations of string solvers. Understand the historical context of string constraints, dating back to Plotkin's work, and explore recent advancements in compression-based methods. Gain insights into the application of string solving in various domains, including Amazon Web Services' Role-Based Access Control policy analysis. Suitable for those interested in programming language theory, software verification, and security, this tutorial aims to demystify the complex world of string constraint solving for the POPL audience.