Vincent Laviron and Francesco Logozzo
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.
|Published in||Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009)|
All copyrights reserved by Springer 2007.
Francesco Logozzo. Our Experience with the CodeContracts Static Checker, Springer, January 2012.
Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.
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.