IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2012 > TVLA and Value Analyses Together

Pietro Ferrara

Tuesday, June 12, 2012

1:00pm IMDEA conference room

Pietro Ferrara, Post-doctoral Researcher, ETH Zurich, Switzerland

TVLA and Value Analyses Together

Abstract:

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.