Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Refining Abstract Interpretation-based Static Analyses with Hints

Vincent Laviron and Francesco Logozzo

Abstract

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.

Details

Publication typeInproceedings
Published in Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009)
PublisherSpringer Verlag

Newer versions

Francesco Logozzo. Our Experience with the CodeContracts Static Checker, Springer, January 2012.

Vincent Laviron and Francesco Logozzo. SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities , International Journal on Software Tools for Technology Transfer (STTT) , Springer Verlag, June 2011.

Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.

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