Abstract interpretation has been widely applied to approximate data structures and (usually numerical) value information, but their combination is needed to effectively apply static analysis to real software. In this context, we introduce a generic framework that, given a heap and a value analysis, combines them, proving formally its soundness. We plug inside this framework a standard allocation site-based pointer analysis, a TVLA-based shape analysis, and standard existing numerical domains. As far as we know, this is the first sound generic automatic framework for statically typed object-oriented programming languages combining heap and value analyses that allows to summarize and materialize heap identifiers.

A generic framework for heap and value analyses of object-oriented programming languages

Ferrara P
2016-01-01

Abstract

Abstract interpretation has been widely applied to approximate data structures and (usually numerical) value information, but their combination is needed to effectively apply static analysis to real software. In this context, we introduce a generic framework that, given a heap and a value analysis, combines them, proving formally its soundness. We plug inside this framework a standard allocation site-based pointer analysis, a TVLA-based shape analysis, and standard existing numerical domains. As far as we know, this is the first sound generic automatic framework for statically typed object-oriented programming languages combining heap and value analyses that allows to summarize and materialize heap identifiers.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/3730030
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 1
social impact