On abstraction refinement for program analyses in Datalog

ABSTRACT

A central task for a program analysis concerns how to efficiently find a program abstraction that keeps only information relevant for proving properties of interest. We present a new approach for finding such abstractions for program analyses written in Datalog. Our approach is based on counterexample-guided abstraction refinement: when a Datalog analysis run fails using an abstraction, it seeks to generalize the cause of the failure to other abstractions, and pick a new abstraction that avoids a similar failure. Our solution uses a boolean satisfiability formulation that is general, complete, and optimal: it is independent of the Datalog solver, it generalizes the failure of an abstraction to as many other abstractions as possible, and it identifies the cheapest refined abstraction to try next. We show the performance of our approach on a pointer analysis and a typestate analysis, on eight real-world Java benchmark programs.

References

1. T. Ball and S. Rajamani. The SLAM project: Debugging system software via static analysis. In POPL, 2002.
2. T. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially quantified Horn clauses. In CAV, 2013.
3. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS, 1999.
4. N. Bjørner, K. McMillan, and A. Rybalchenko. On solving universally quantified Horn clauses. In SAS, 2013.
5. M. Bravenboer and Y. Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In OOPSLA, 2009.
6. S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In ICSE, 2003.
7. E. Clarke, A. Gupta, J. Kukula, and O. Shrichman. SAT based abstraction-refinement using ILP and machine learning techniques. In CAV, 2002.
8. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. JACM, 50 (5), 2003.
9. S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ACM TOSEM, 17(2), 2008.
10. S. Grebenshchikov, A. Gupta, N. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A software verifier based on Horn clauses. In TACAS, 2012.
11. T. Henzinger, R. Jhala, R. Majumdar, and K. McMillan. Abstractions from proofs. In POPL, 2004.
12. K. Hoder, N. Bjørner, and L. de Moura. μZ - an efficient engine for fixed points with constraints. In CAV, 2011.
13. M. Janota. MiFuMax --- a literate MaxSat solver, 2013.
14. B. Jaumard and B. Simeone. On the complexity of the maximum satisfiability problem for Horn formulas. IPL, 26(1):1--4, 1987.
15. G. Kastrinis and Y. Smaragdakis. Hybrid context sensitivity for points-to analysis. In PLDI, 2013.
16. O. Lhoták and L. Hendren. Jedd: a BDD-based relational extension of Java. In PLDI, 2004.
17. P. Liang and M. Naik. Scaling abstraction refinement via pruning. In PLDI, 2011.
18. V. Manquinho, J. M. Silva, and J. Planes. Algorithms for weighted boolean optimization. In SAT, 2009.
19. A. Milanova, A. Rountev, and B. Ryder. Parameterized object sensitivity for points-to and side-effect analyses for Java. In ISSTA, 2002.
20. J. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th Intl. Symp. on Programming, 1982.
21. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, 1995.
22. Y. Smaragdakis and M. Bravenboer. Using Datalog for fast and easy program analysis. In Datalog 2.0 Workshop, 2010.
23. Y. Smaragdakis, M. Bravenboer, and O. Lhoták. Pick your contexts well: Understanding object-sensitivity. In POPL, 2013.
24. J. Whaley and M. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI, 2004.
25. J. Whaley, D. Avots, M. Carbin, and M. Lam. Using Datalog with binary decision diagrams for program analysis. In APLAS, 2005.
26. X. Zhang, M. Naik, and H. Yang. Finding optimum abstractions in parametric dataflow analysis. In PLDI, 2013.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification