Abstract domains in 3D: completeness and refinements in static
program analysis and abstract model checking


In this talk we will give a survey on recent results
in systematic abstract domain design for program analysis.
We introduce a framework for studing
abstract domain transformers, in particular domain
refinements, domain compressors and domain simplification
operators. The idea is to lift standard abstract interpretation
theory one level up, where the objects of abstraction are not
the objects computed by a program but rather the abstract domains
themselves. In this way we are able to systematically design
operations that act on abstract domain to improve, reduce, and
simplify their precision. The notion of completeness plays
a key role in this theory. We prove that most abstract domain
transformers can be viewed as instances of the problem of
transforming a domain in order to achieve completeness
with respect to a given function. This theory has been
applied to systematically design abstract domain transformers
in order to refine static program analysis and abstract
model checking.