TVAL+: Combining TVLA and Value Analyses

Effective static analyses have to deal with the approximation of the heap structure and the information about values. In the field of heap abstraction, shape analysis has obtained great achievements during the last decade. Similarly, numerical and other value abstractions obtained great results, and they are nowadays effectively applied to the analysis of industrial software. In addition, several generic static analyzers have been developed. These analyzers combine various abstractions into the same analysis.

In this talk, we will present TVAL+, the combination of Sample, an existing generic analyzer, with a TVLA-based heap abstraction. First of all, we will define how Sample splits the heap abstraction from the value analysis. We will then present how TVLA states are augmented with name predicates to identify nodes, and how these predicates are used to track the merge and materialization of nodes. Finally, we will sketch some preliminary experimental results.

Speaker Details

Pietro Ferrara is a postdoc at ETH Zurich in the Chair of Programming Methodology. His research focuses on static analysis via abstract interpretation, and in particular on the formalization and development of generic analyzers for object oriented programs. He received a Ph.D. from the Ecole Polytechnique and the University “Ca’ Foscari” of Venice in 2009. He has been an intern at Microsoft Research in Redmond in 2007

Series:
Microsoft Research Talks
Date:
Speakers:
Pietro Ferrara
Affiliation:
ETH Zurich

Series: Microsoft Research Talks