Synthesizing Specifications

This paper studies how to synthesize useful formal specifications from program code. Instead of requiring a developer to manually write every property, the framework takes a query about a set of function definitions and a domain-specific language for expressing candidate properties.

The synthesized results are best properties in the chosen language: each property is as precise as possible within the language, and the set is exhaustive with respect to the query. This makes the approach useful for extracting program facts that are both formal and tailored to the kind of property a user wants to see.

The work is implemented in Spyro and demonstrates applications including program-specification mining, abstract-domain operations, and algebraic properties of program modules. It appeared at OOPSLA 2023.