Skip to main content

On abstraction refinement for program analyses in Datalog

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

PDF - Publisher pdf
Download (342kB) Preview
Official URL


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: Conference or workshop item (Paper)
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: 29 May 2019 17:00 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year