Petablox: Declarative Program Analysis for Big Code

Most software development today leverages the world's massive collection of open source software. There is significant room for program analyses to similarly leverage Big Code, the collective knowledge amassed from analyzing existing programs, to automatically infer or predict salient behaviors and vulnerabilities in new programs. Petablox is a framework for automatically synthesizing use-cases of arbitrary declarative program analyses for Big Code tasks such as efficiently finding good abstractions, transferring analysis results across programs, and adapting analyses to user feedback. Despite their diversity, all these tasks entail solving large instances of MaxSAT, the maximum satisfiability problem which comprises a mix of hard (inviolable, logical) constraints and soft (violable, probabilistic) constraints. Petablox encompasses demand-driven, compositional, and learning-based MaxSAT optimizations for scaling these tasks to large code bases.

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.