Theory of Domain Design in Abstract Interpretation Seminars/Workshops

Abstract

In this mini course we introduce a general theory of domain operations for the systematic design of abstract domains and program analyses. The mini course is in 3 parts. In the first part we will consider the problem of making abstract domains complete with respect to a given semantics function. The solution of this problem gives us the theoretical basis for designing a theory of domain operations for refining and simplifying domains in abstract interpretation, which is developed in the second part of the course. In the third part we close the picture by studying the structure of domain compressors. Domain compressors can also be viewed as instances of the same framework based on the notion of completeness. The whole final picture should provide a unfifying theory for domain operations in abstract interpretation which should assist in the systematic design of abstract interpreters for automatic program analysis.

[8/26 10am KAIST 전산동 1403]
Part I: Complete abstract interpretations made constructive
Abstract: We prove that any domain can be extended and reduced into respectively the most abstract and concrete domain which is complete for a given semantic function. Completeness means here that no additional loss of information is obtained by computing in the abstract domain with respect to abstracting the concrete computation. We provide constructive methods for designing these domains and discuss applications in functional and logic program analysis.

[8/27 10am KAIST 전산동 1403]
Part II: The structure of domain operations in abstract interpretation: Domain refinement and simplification
Abstract: Based on the theory developed in the first part, we show that all known domain operations for enhancing/reducing the precision of abstract domains can be formulated as completeness problems with respect to suitable functions. The constructive characterization of the solution of this problem provides advanced methods for designing domain operations in abstract interpretation.

[8/27 10am KAIST 전산동 1403]
Part III: The structure of domain operations in abstract interpretation: Domain compression
Abstract: We introduce the notion of domain compression as a generalization of domain complementation and disjunctive bases introduced by the author. This notion can be studied in the above mentioned framework as an instance of suitable completeness problems. The talk will be closed by a global picture where all domain operations are represented in a geometrical structure. We will discuss also the possible impact of this theory in the systematic design of domains for program analysis.