Automata Based String Analysis

In this chapter, we discuss using automata as a symbolic representation for string analysis. To compute forward and backward reachability for string manipulating programs, we can use automata-based symbolic string analysis where automata are used as a symbolic representation to represents sets of states of the program. We can iteratively compute an approximation of the least fixpoint that corresponds to the reachable values of the string expressions. Assume that we use one Deterministic Finite Automaton (DFA) per string variable, per program point. I.e., each DFA represents the set of values that a string variable can take at a particular program point. In each iteration, given the current state DFA for a variable, we can compute the pre- and post-state DFA. In order to implement this approach we have to develop automata based algorithms for computing pre- and post-state computation for common string …