M-String Segmentation: a refined abstract domain for static analysis of C programs.

The goal of the thesis is to present a refined segmentation abstract domain for the analysis of strings in C programming language. We properly extend the parametric segmentation approach to array representation by P. Cousot to the case of text values. In particular, we capture the so-called “string of interest” of an array of char, and we are able to distinguish well-formed string arrays. A concrete and abstract semantics of the main C header file string.h functions are presented in full detail.