Mayur Naik
ABSTRACT
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%.
Supplemental Material
- T. Ball and S. Rajamani. The slam project: Debugging system software via static analysis. In POPL, pages 1--3, 2002. Google Scholar
Digital Library
- N. E. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons. Proofs from tests. In ISSTA, pages 3--14, 2008. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In PLDI, pages 300--309, 2007. Google ScholarDigital Library
- VanDrunen, von Dincklage, and Wiedermann}dacapoS. M. Blackburn, R. Garner, C. Hoffman, A. M. Khan, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, J. E. B. Moss, A. Phansalkar, D. Stefanović, T. VanDrunen, D. von Dincklage, and B. Wiedermann. The DaCapo benchmarks: Java benchmarking development and analysis. In OOPSLA, pages 169--190, 2006. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. JACM, 50 (5), 2003. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In POPL, pages 238--252, 1977. Google ScholarDigital Library
- C. Csallner and Y. Smaragdakis. Check 'n' Crash: combining static checking and testing. In ICSE, pages 422--431, 2005. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. Dart: directed automated random testing. In PLDI, pages 213--223, 2005. Google ScholarDigital Library
- P. Godefroid, A. Nori, S. Rajamani, and S. Tetali. Compositional may-must program analysis: unleashing the power of alternation. In POPL, pages 43--56, 2010. Google ScholarDigital Library
- B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. Synergy: a new algorithm for property checking. In SIGSOFT FSE, pages 117--127, 2006. Google ScholarDigital Library
- A. Gupta, R. Majumdar, and A. Rybalchenko. From tests to proofs. In TACAS, pages 262--276, 2009. Google ScholarDigital Library
- S. Guyer and C. Lin. Client-driven pointer analysis. In SAS, pages 214--236, 2003. Google ScholarDigital Library
- T. Henzinger, R. Jhala, R. Majumdar, and K. McMillan. Abstractions from proofs. In POPL, pages 232--244, 2004. Google ScholarDigital Library
- P. Liang and M. Naik. Scaling abstraction refinement via pruning. In PLDI, pages 590--601, 2011. Google ScholarDigital Library
- P. Liang, O. Tripp, and M. Naik. Learning minimal abstractions. In POPL, pages 31--42, 2011. Google ScholarDigital Library
- K. McMillan. Relevance heuristics for program analysis. In POPL, pages 145--146, 2008. Google ScholarDigital Library
- A. V. Nori, S. K. Rajamani, S. Tetali, and A. V. Thakur. The yogi project: Software property checking via static analysis and testing. In TACAS, pages 178--181, 2009. Google ScholarDigital Library
- J. Plevyak and A. Chien. Precise concrete type inference for object-oriented languages. In OOPSLA, pages 324--340, 1994. Google ScholarDigital Library
- J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proceedings of the 5th International Symposium on Programming, pages 337--350, 1982. Google ScholarDigital Library
- N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. A semantics for procedure local heaps and its abstractions. In POPL, pages 296--309, 2005. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. Cute: a concolic unit testing engine for c. In FSE, pages 263--272, 2005. Google ScholarCross Ref
- G. Yorsh, T. Ball, and M. Sagiv. Testing, abstraction, theorem proving: Better together! In ISSTA, pages 145--156, 2006. Google ScholarDigital Library
Index Terms
- Abstractions from tests
Recommendations
Abstractions from tests
POPL '12We 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 ...
Side-effect analysis with fast escape filter
SOAP '12: Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program analysisSide-effect analysis is a fundamental static analysis used to determine the memory locations modified or used by each program entity. For the programs with pointers, the analysis can be very imprecise. To improve the precision of side-effect analysis, ...
Introspective analysis: context-sensitivity, across the board
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationContext-sensitivity is the primary approach for adding more precision to a points-to analysis, while hopefully also maintaining scalability. An oft-reported problem with context-sensitive analyses, however, is that they are bi-modal: either the analysis ...
Comments