A²I: Abstract² interpretation

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.