Petablox: Declarative Program Analysis for Big Code

Big Code, the collective knowledge amassed from analyzing programs, presents a timely and unprecedented opportunity to improve existing methods for program reasoning and enable newer ones. Petablox is a new declarative paradigm and system that aims to serve as a foundation to realize this objective. Based on the logic programming language Datalog, Petablox addresses challenges of application diversity and implementation complexity in seeking a broad and deep unification that has eluded past declarative efforts in program analysis. Starting from a single common specification of any program analysis in Datalog, it automatically synthesizes Big-Code tasks such as tailoring program abstractions to analysis queries, transferring analysis facts across programs, and incorporating user feedback to improve analysis results over time.

This research is funded in part by DARPA as part of the MUSE program (contract #FA8750-15-2-0009) and by NSF Award New Frontiers in Constraint-Based Program Analysis.