A Taxonomy of Program Analyses

The design of static analyses of programs in the abstract interpretation theory starts with the choice of a collecting semantics, which is the strongest property we can derive for a program. Starting from well-known collecting semantics for functional programs in the literature, we propose a taxonomy of program properties by considering the sets of abstract interpretations for which the collecting semantics is initial and show that they can be constructively characterized in terms of the abstraction functions.