AbstractGiven a specification $\varphi(X,Y)$ over inputs $X$ and output $Y$, defined over a background theory $\mathbb{T}$, the problem of
program synthesis is to design a program $f$ such that $Y=f(X)$ satisfies the specification $\varphi$. Over the past decade,
→