SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers

TL;DR

SynRG introduces a novel synthesis algorithm that handles complex specifications involving quantifiers and alternations by restricting and generalizing solutions, outperforming existing solvers on benchmark problems.

Contribution

The paper presents SynRG, a new synthesis method that effectively manages quantifier alternations in unbounded data structures, advancing the state-of-the-art in program synthesis.

Findings

Successfully synthesizes complex expressions with quantifier alternations.

Outperforms existing solvers on invariant and program sketching benchmarks.

Effective on benchmarks from Java StringUtils class.

Abstract

Program synthesis is the task of automatically generating expressions that satisfy a given specification. Program synthesis techniques have been used to automate the generation of loop invariants in code, synthesize function summaries, and to assist programmers via program sketching. Syntax-guided synthesis has been a successful paradigm in this area, however, one area where the state-of-the-art solvers fall-down is reasoning about potentially unbounded data structures such as arrays where both specifications and solutions may require quantifiers and quantifier alternations. We present SynRG, a synthesis algorithm based on restricting the synthesis problem to generate candidate solutions with quantification over a finite domain, and then generalizing these candidate solutions to the unrestricted domain of the original specification. We report experiments on invariant synthesis benchmarks and on program sketching benchmarks taken from the Java StringUtils class and show that our technique can synthesize expressions out of reach of all existing solvers.