Abstractions from Tests

作者：Naik Mayur^*; Yang Hongseok; Castelnuovo Ghila; Sagiv Mooly

来源：ACM Sigplan Notices, 2012, 47(1): 373-385.

DOI：10.1145/2103621.2103701

• Languages
• Verification
• Parametrised Static Analysis
• Testing
• Thread-Escape Analysis
• Points-to Analysis
• Necessary-Condition Problem

We present a framework for leveraging dynamic analysis to find good abstractions for static analysis. A static analysis in our framework is parametrised. Our main insight is to directly and efficiently compute from a concrete trace, a necessary condition on the parameter configurations to prove a given query, and thereby prune the space of parameter configurations that the static analysis must consider. We provide constructive algorithms for two instance analyses in our framework: a flow- and context-sensitive thread-escape analysis and a flow-and context-insensitive points-to analysis. We show the efficacy of these analyses, and our approach, on six Java programs comprising two million bytecodes: the thread-escape analysis resolves 80% of queries on average, disproving 28% and proving 52%; the points-to analysis resolves 99% of queries on average, disproving 29% and proving 70%.

• 出版日期2012-1