SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers

07/20/2020
by   Elizabeth Polgreen, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset