Refining Abstract Interpretation-based Static Analyses with Hints

The existing approaches for refining static analyses focus on the refinement either of the elements of abstract domains or of the transfer functions.

Here, we focus our attention on the loss of precision induced by abstract domain operations.

We introduce a new technique, hints, which allows to systematically refine the operations defined over elements of an abstract domain.

We formally define hints in the abstract interpretation theory, we prove their soundness, and we characterize two families of hints: syntactic and semantic.

We give some examples of hints, and we provide our experience with hints in Clousot, our abstract interpretation-based static analyzer for NET.

Hints.pdf
PDF file

In   Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009)

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

TypeInproceedings
> Publications > Refining Abstract Interpretation-based Static Analyses with Hints