review articles
Writing programs that are both correct and efficient is
challenging. A potential solution lies in program
synthesis aimed at automatic derivation of an
executable implementation (the “how”) from a high-level logical specification of the desired input-to-output behavior (the “what”). A mature synthesis
technology can have a transformative impact on
programmer productivity by liberating the programmer
from low-level coding details. For instance, for the
classical computational problem of sorting a list of
numbers, the programmer has to simply specify that
given an input array A of n numbers, compute an
output array B consisting of exactly the same numbers
as A such that B[i] ≤ B[i + 1] for 1 ≤ i < n, leaving it to the
synthesizer to figure out the sequence of steps needed
for the desired computation.
Traditionally, program synthesis is formalized as
a problem in deductive theorem proving: 17 A program
is derived from the constructive proof of the theorem
that states that for all inputs, there ex-
ists an output, such that the desired
correctness specification holds.
Building automated and scalable
tools to solve this problem has proved
to be difficult. A recent alternative to
formalizing synthesis allows the pro-
grammer to supplement the logical
specification with a syntactic tem-
plate that constrains the space of al-
lowed implementations and the solu-
tion strategies focus on search
algorithms for efficiently exploring
this space. The resulting search-based
program synthesis paradigm is emerg-
ing as an enabling technology for
both designing more intuitive pro-
gramming notations and aggressive
program optimizations.
As an instance of making program-
ming easier and accessible to end
users, consider the programming-by-
examples (PBE) systems that allow a
user to specify the desired functional-
ity using representative input-to-out-
put examples. Such a programming
environment is feasible in domain-
specific applications such as data
manipulation as illustrated by the
success of the FlashFill feature in
Microsoft Excel spreadsheet soft-
ware. 10, 11 This feature can automati-
cally fill in a column in the spreadsheet
by examining a few examples pro-
vided by the user. The underlying
computational problem is search-
based synthesis, namely, finding a
program that is consistent with all the
user-provided examples and fits the
syntactic template of the native
language.
Search-based
Program
Synthesis
DOI: 10.1145/3208071
A promising, useful tool for future
programming development environments.
BY RAJEEV ALUR, RISHABH SINGH,
DANA FISMAN, AND ARMANDO SOLAR-LEZAMA
key insights
˽ Syntex-guided synthesis formalizes the
computational problem of searching for
a program expression that meets both
syntactic and logical constraints.
˽ A wide variety of problems, such as
programming by examples, program
superoptimization, and program repair,
naturally map to syntax-guided synthesis.
˽ Standardization, benchmark collection,
and solver competition have led
to significant advances in solution
strategies and new applications. IM
A
G
E
F
R
O
M
S
H
U
T
T
E
R
S
T
O
C
K
.
C
O
M
