Synthesizing Program-Specific Static Analyses

TL;DR

This paper introduces a method for synthesizing program-specific static analyses using example-based approaches, reducing the need for expert knowledge and development resources in creating tailored program analyses.

Contribution

It presents a novel approach to automatically generate program-specific static analyses from developer-provided examples within familiar domains.

Findings

Enables synthesis of analyses from simple developer examples

Reduces reliance on expert knowledge and extensive development

Applicable to domains like type qualifiers and effect systems

Abstract

Designing a static analysis is generally a substantial undertaking, requiring significant expertise in both program analysis and the domain of the program analysis, and significant development resources. As a result, most program analyses target properties that are universallly of interest (e.g., absence of null pointer dereference) or nearly so (e.g., deadlock freedom). However, many interesting program properties that would benefit from static checking are specific to individual programs, or sometimes programs utilizing a certain library. It is impractical to devote program analysis and verification experts to these problems. We propose instead to work on example-based synthesis of program analyses within well-understood domains like type qualifier systems and effect systems. The dynamic behaviors behind the classes of problems these systems prevent correspond to examples that developers who lack expertise in static analysis can readily provide (data flow paths, or stack traces).