A^2 I: Abstract^2 Interpretation

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 Astree 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 ars 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.