On the Concept of Variable Roles and its Use in Software Analysis
This work addresses a gap in formal methods for software verification, though it is incremental as it builds on existing data flow analysis techniques.
The paper tackles the problem of systematically classifying variable roles in C code, which are important for software analysis but not formally studied, and demonstrates its method by predicting file categories in the SVCOMP 2013 competition.
Human written source code in imperative programming languages exhibits typical patterns for variable use such as flags, loop iterators, counters, indices, bitvectors etc. Although it is widely understood by practitioners that these variable roles are important for automated software analysis tools, they are not systematically studied by the formal methods community, and not well documented in the research literature. In this paper, we study the notion of variable roles on the example of basic types (int, float, char) in C. We propose a classification of the variables in a program by variable roles, and demonstrate that classical data flow analysis lends itself naturally both as a specification formalism and an analysis paradigm for this classification problem. We demonstrate the practical applicability of our method by predicting membership of source files to the different categories of the software verification competition SVCOMP 2013.