String Constraints with Concatenation and Transducers Solved Efficiently

Watch a 17-minute conference presentation from POPL 2018 exploring an efficient approach to solving string constraints with concatenation and transducers. Learn how researchers developed the first string solver capable of handling both concatenation and finite-state transductions, with guaranteed completeness and termination for key fragments like straight-line code. Discover how the team tackled the double-exponential time complexity challenge by utilizing succinct alternating finite-state automata as symbolic representations of string constraints. Understand the practical applications in cross-site scripting detection and automatic test-case generation, particularly for analyzing web application sanitization functions and browser transductions. See how model checking algorithms like IC3 are employed for state-space exploration in exponential-sized graphs, with implementation results demonstrating the solver's effectiveness on real-world benchmarks.