Semantics-Guided Synthesis

TL;DR

This paper introduces SemGuS, a flexible framework for program synthesis that incorporates user-defined syntax and semantics, enabling the synthesis and proof of unrealizability for complex imperative programs with unbounded loops.

Contribution

It presents SemGuS, a novel semantics-guided synthesis framework, and an algorithm that encodes synthesis problems as proof searches over Constrained Horn Clauses, capable of handling unbounded loops.

Findings

First to prove unrealizability for imperative programs with unbounded loops.

Successfully applied to SyGuS and imperative language synthesis problems.

Implemented in the MESSY tool for practical use.

Abstract

This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuS framework, we develop an algorithm for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, our approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space. We implemented the technique in a tool called MESSY, and applied it to both SyGuS problems(i.e., over expressions) and synthesis problems over an imperative programming language.