IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2012 > TVLA and Value Analyses Together
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Pietro Ferrara

martes 12 de junio de 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.