Abstract
We focus our attention on the loss of precision induced by abstract domain operations. We introduce a new technique, hints, which allows us 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. © 2009 Springer-Verlag.
Cite
CITATION STYLE
Laviron, V., & Logozzo, F. (2009). Refining abstract interpretation-based static analyses with hints. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5904 LNCS, pp. 343–358). https://doi.org/10.1007/978-3-642-10672-9_24
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
