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

@article{paperbot636,
  title = {A²I: abstract² interpretation},
  author = {Patrick Cousot and Roberto Giacobazzi and Francesco Ranzato},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3290355}
}