On abstraction refinement for program analyses in Datalog

Radu Grigore

Static analyzers still face significant challenges in coping with large programs. And, of course, developers want their queries about the code answered quickly. I will present a CEGAR-based approach that enables analyzers to scale better. The assumptions being made are rather weak:

  1. the analyzer is implemented in Datalog, and
  2. its precision can be finely tuned.
However, the following problem can be solved completely automatically: Tune the precision of the analyzer to solve a given query. One of the main ingredients of the solution is a MAXSAT solver.

This is joint work with Xin Zhang, Ravi Mangal, Mayur Naik, and Hongseok Yang.