Skip to main content

On abstraction refinement for program analyses in Datalog

Zhang, Xin and Mangal, Ravi and Grigore, Radu and Naik, Mayur and Yang, Hongseok (2014) On abstraction refinement for program analyses in Datalog. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI Programming Language Design and Implementation . ACM, New York, USA, pp. 239-248. ISBN 978-1-4503-2784-8. (doi:10.1145/2594291.2594327)

PDF - Publisher pdf
Download (342kB) Preview
[img]
Preview
Official URL
http://dx.doi.org/10.1145/2594291.2594327

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.

Item Type: Book section
DOI/Identification number: 10.1145/2594291.2594327
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Radu Grigore
Date Deposited: 12 Feb 2016 11:21 UTC
Last Modified: 23 Sep 2019 11:29 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/54177 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year