Constraint-Based String Analysis

Abstract

Analysis of string manipulating programs has been studied extensively in recent years. One of the commonly used program analysis technique, symbolic execution, can be applied to string manipulating programs. However, symbolic execution of string manipulating programs is difficult since solving string constraints is a challenging problem. String constraint solving is challenging due to two main reasons: 1) With the increasing usage of strings in modern software development, programming languages provide increasingly complex string operations that need to be handled by string constraint solvers. 2) String constraints are usually mixed with integer constrains which requires solving integer constraints together with string constraints. In this chapter, we first provide an illustrative example of the symbolic execution of a string manipulating program. Then, we discuss the details of automata-based constraint solving and model counting extension to string constraint solving.