Semantics-Guided Synthesis

Semantics-guided synthesis (SemGuS) is a framework for specifying arbitrary synthesis problems. SemGuS 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.

SemGuS Format v1.0

Benchmarks and Solvers

Publications and Talks

Semantics-Guided Synthesis. Jinwoo Kim, Qinheping Hu, Loris D’Antoni, and Thomas Reps. 2021.

A 5-minute talk on Semantics-Guided Synthesis.

Contact Us

Contact Jinwoo Kim with any questions or comments.

The SemGuS Team