Lifting String Analysis Domains

Strings are characterized by properties that either refer to their content (e.g., the set of contained characters) and to their shape (e.g., the character position and the length of the strings). In this paper, we present a general framework providing a systematic lifting of string domains through a segmentation abstraction, yielding to a more accurate representation of strings without major impact on efficiency of the analysis. The proposed operator exploits the abstraction functor introduced by Cousot, Cousot and Logozzo for a fully parametric array representation, in the string scenario.