TVLA and Value Analyses Together

June 12, 2012

Pietro Ferrara


TVLA and Value Analyses Together

Time:   1:00pm
Location:   IMDEA conference room

Effective static analyses must precisely approximate both heap structure and information about values. During the last decade, shape analysis has obtained great achievements in the field of heap abstraction. Similarly, numerical and other value abstractions have made tremendous progress, and they are nowadays effectively applied to the analysis of industrial software. In addition, several generic static analyzers have been introduced. These compositional analyzers combine many types of abstraction into the same analysis to prove various properties.

In this talk, we will present the combination of Sample, an existing generic analyzer, with a TVLA-based heap abstraction. First of all, we will introduce how Sample splits the heap abstraction from the value analysis. We will then present how we augment TVLA states with name predicates to identify nodes, and how we use TVLA as the engine to define the small step semantics of our analysis. Finally, we will sketch some preliminary experimental results.