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.