Theory of Domain Design in Abstract Interpretation Seminars/Workshops
|Time:||1999-08-26 10:00:001999-08-27 10:00:001999-08-28 10:00:00|
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.
[ List ]