Bao-Quan Cui

Solving String Split Constraints via Structural Relaxation

String operations are integral to program analysis, yet reasoning about the ubiquitous split operation remains a challenge. SMT solvers have difficulty with split because it transforms a string into a variable-length sequence, creating a structural mismatch that leads to uninterpreted abstractions or unsound bounded ap...