The fundamental idea of Abstract2 Interpretation (A2I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A2I is generally meant to use abstract interpretation to analyse properties of program analysers. A2I can be either offline or online. Offline A2I is performed either before the program analysis, such as variable packing used by the Astrée program analyser, or after the program analysis, such as in alarm diagnosis. Online A2I is performed during the program analysis, such as Venet’s cofibred domains or Halbwachs et al.’s and Singh et al.’s variable partitioning techniques for fast polyhedra/numerical abstract domains. We formalize offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.

A²I: abstract² interpretation

COUSOT, PATRICK MARCEL PAUL MAURICE;GIACOBAZZI, ROBERTO;Ranzato, Francesco
2019

Abstract

The fundamental idea of Abstract2 Interpretation (A2I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A2I is generally meant to use abstract interpretation to analyse properties of program analysers. A2I can be either offline or online. Offline A2I is performed either before the program analysis, such as variable packing used by the Astrée program analyser, or after the program analysis, such as in alarm diagnosis. Online A2I is performed during the program analysis, such as Venet’s cofibred domains or Halbwachs et al.’s and Singh et al.’s variable partitioning techniques for fast polyhedra/numerical abstract domains. We formalize offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.
File in questo prodotto:
File Dimensione Formato  
published-paper.pdf

accesso aperto

Descrizione: ACM version
Tipologia: Published (publisher's version)
Licenza: Creative commons
Dimensione 571.63 kB
Formato Adobe PDF
571.63 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS 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/11577/3288990
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 10
social impact