Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato. A2I: abstract2 interpretation.

Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato.
A²I: abstract² interpretation.
In Proceedings of the ACM on Programming Languages: Volume 3 Issue POPL, Article No. 42, January 2019, 31 pages. https://doi.org/10.1145/3290355, Cascais, Portugal, January 16—18, 2019. © ACM Press, New York.
Letter paper format: PDF (586 KB) (proofs (279 KB))

Distinguished paper award: PDF (586 KB)

CCS Concepts:
- Software and its engineering → Automated static analysis; Formal software verification; Semantics;
- Theory of computation → Program analysis.

Keywords: Abstract interpretation, Meta-abstract interpretation, Program analysis.

Abstract: The fundamental idea of Abstract² Interpretation (A²I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A²I is generally meant to use abstract interpretation to analyse properties of program analysers. A²I can be either offline or online. Offline A²I 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 A²I 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.

Slides: Keynote (5.1 MB), PDF (2.6 MB), recording (85.4 MB),

Bibliographic reference:

@article{DBLP:journals/pacmpl/CousotGR19,
  author    = {Patrick Cousot and
               Roberto Giacobazzi and
               Francesco Ranzato},
  title     = {A{\({^2}\)}I: abstract{\({^2}\)} interpretation},
  journal   = {{PACMPL}},
  volume    = {3},
  number    = {{POPL}},
  pages     = {42:1--42:31},
  year      = {2019}
}

Copyright: © ACM, (2019). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in the Proceedings of the ACM on Programming Languages: Volume 3 Issue POPL, January 2019. Copyright © 2019 ACM.

copyright notice, ACM copyright
Last modified: Saturday, 16-Mar-2019 18:20:59 EDT