String Abstractions for String Verification
Verifying string manipulating programs is a crucial problem in computer security. String operations are used extensively within web applications to manipulate user input, and their erroneous use is the most common cause of security vulnerabilities in web applications. Unfortunately, verifying string manipulating programs is an undecidable problem in general and any approximate string analysis technique has an inherent tension between efficiency and precision. In this paper, the authors present a set of sound abstractions for strings and string operations that allow for both efficient and precise verification of string manipulating programs.