Synthesizing Specifications

TL;DR

The paper tackles automatic synthesis of precise specifications by introducing a customizable framework that takes a query $\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\ {\\Phi}$ and a user-defined DSL $\ {\\mathcal{L}}$ to produce a best $\ {\\mathcal{L}}$-conjunction. It advances a counterexample-guided inductive synthesis approach that constructs incomparable best $\ {\\mathcal{L}}$-properties using positive and negative examples, with formal guarantees of soundness and precision under suitable language-structure assumptions. The authors implement Spyro in two modes (SMT-based and Sketch-based) and evaluate it on four applications: specification mining, modular algebraic specifications, sensitivity analysis, and enabling new abstract domains, demonstrating substantial performance and qualitative benefits, including discovering real bugs in modules. Overall, the work provides a flexible, provably correct pathway to extract highly precise, reusable specifications from code, with broad practical impact for verification, synthesis, and abstract interpretation.

Abstract

Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: i) a query posed about a set of function definitions, and ii) a domain-specific language L in which the extracted property is to be expressed (we call properties in the language L-properties). Each of the property is a best L-property for the query: there is no other L-property that is strictly more precise. Furthermore, the set of synthesized L-properties is exhaustive: no more L-properties can be added to it to make the conjunction more precise. We implemented our method in a tool, Spyro. The ability to modify both the query and L provides a Spyro user with ways to customize the kind of specification to be synthesized. We use this ability to show that Spyro can be used in a variety of applications, such as mining program specifications, performing abstract-domain operations, and synthesizing algebraic properties of program modules.

Figures (8)

• Figure 1: The role of examples and CheckSoundness.
• Figure 2: Possible results produced by CheckPrecision
• Figure 3: $\mathcal{L}$-properties synthesized by spyro. Some properties are rewritten as implications for readability.
• Figure 4: Each subfigure illustrates a bit-vector formula (in green) and the most precise bit-vector polyhedron computed by spyro (i.e., the inequalities above the formulas). Each colored cell in the plots represents a solution in $4$-bit unsigned modular arithmetic of the conjunction of the inequalities found by spyro: green cells represent solutions to the original formula, whereas red cells are points that are solution to the inequalities, but do not satisfy the original formula. In (a) and (b), the conjunctive formula represents the original formula exactly (there are only green cells). In (b), the twelve occurrences of red cells are points that do not satisfy the original formula, but are needed for a conjunctive formula to over-approximate the original formula.
• Figure 5: Evaluation of the running time of spyro for different input sizes and optimizations.

Theorems & Definitions (23)

• Definition 2.1: A best $\mathcal{L}$-property
• Definition 2.2: Best $\mathcal{L}$-conjunction
• theorem 1
• Definition 2.3: Problem definition
• Example 2.1: Infinite $\mathcal{L}$-conjunction
• Definition 3.1: Examples
• Example 3.1
• Example 3.2
• Example 3.3: CheckSoundness
• Example 3.4: CheckPrecision