Abstract

Recent years have witnessed widespread use of Datalog in expressing program analyses—programs that infer useful facts about other programs. Examples include analyses for proving security and concurrency properties of imperative programs. The benefits of Datalog, however, are currently limited to automating low-level implementation issues, such as efficient data structures and algorithms for executing these analyses. In particular, the task of finding an effective program abstraction—a central task that concerns balancing the scalability and accuracy of an analysis—is done manually by analysis designers. I will describe a new technique that lifts this limitation. The technique is based on counterexample-guided abstraction refinement which was developed in the model-checking community. When a run of a Datalog analysis fails to prove a program fact using the current abstraction, our technique generalizes the cause of the failure to other abstractions, and picks a new abstraction that avoids a similar failure. It uses a boolean satisfiability solver for this purpose in a manner that is general, complete, and optimal. I will discuss our experience applying this technique in the Chord framework to analyze real-world Java programs.