June 19, 2018
Isabel García
Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis soundness and termination, but they also imply that the analysis is not guaranteed to always produce useful results. In such cases it is necessary to have some means for users to provide information to guide analysis and thus to improve precision, such as the trust assertions of CiaoPP or the “known facts” of Astrée. This allows dealing with, e.g., predicates for which the analysis is not complete or when the source is only partially available. We present techniques for supporting within an abstract interpretation framework with a rich set of trust assertions (conditional, dealing with call/success pairs and multivariance). We extend the language of program-point assertions to deal with multi-variance. Our techniques can also deal with the cases where run-time checks for assertions are present in the program and those in which no run-time checks are generated. Finally, we show how the approach can be applied to both improving precision and accelerating.