AG 2   Info

AG Audience

-- Not specified --

Saarbrücken

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.

--email hidden

passcode not visible

logged in users only