Information Technology Reference
In-Depth Information
Synthesis with input/output examples.
One of the first works that addressed
synthesis with examples and put inductive synthesis on a firm theoretical foun-
dation is the one by Summers [66]. Subsequent work presents extensions of the
classical approach to induction of functional Lisp-programs [
?
,30]. These ex-
tensions include synthesizing a set of equations (instead of just one), multiple
recursive calls and systematic introduction of parameters. Our current system
lifts several restrictions of previous approaches by supproting reasoning about
arbitrary datatypes, supporting multiple parameters in concrete and symbolic
I/O examples, and allowing nested recursive calls and user-defined declarations.
Inductive programming and programming by demonstration.
Inductive (logic)
programming that explores automatic synthesis of (usually recursive) programs
from incomplete specifications, most often being input/output examples [24,49],
influenced our work. Recent work in the area of programming by demonstration
has shown that synthesis from examples can be effective in a variety of domains,
such as spreadsheets [60]. Advances in the field of SAT and SMT solvers inspired
counter-example guided iterative synthesis [27,64], which can derive input and
output examples from specifications. Our tool uses and advances these techniques
through two new counterexample-guided synthesis approaches.
Synthesis based on finitization techniques.
Program sketching has demonstrated
the practicality of program synthesis by focusing its use on particular domains
[62-64]. The algorithms employed in sketching are typically focused on appropri-
ately guided search over the syntax tree of the synthesized program. The tool we
presented shows one way to move the ideas of sketching towards infinite domains.
In this generalization we leverage reasoning about equations as much as SAT tech-
niques.
Reactive synthesis.
Synthesis of reactive systems generates programs that run
forever and interact with the environment. However, known complete algorithms
for reactive synthesis work with finite-state systems [55] or timed systems [4].
Such techniques have applications to control the behavior of hardware and em-
bedded systems or concurrent programs [73]. These techniques usually take spec-
ifications in a fragment of temporal logic [54] and have resulted in tools that can
synthesize useful hardware components [33, 34]. Recently such synthesis tech-
niques have been extended to repair that preserves good behaviors [23], which is
related to our notion of partial programs that have remaining
choose
statements.
Automated inference of program fixes and contracts.
These areas share the
common goal of inferring code and rely on specialized software synthesis tech-
niques [53,74,75]. Inferred software fixes and contracts are usually snippets of
code that are synthesized according to the information gathered about the an-
alyzed program. The core of these techniques lies in the characterization of
runtime behavior that is used to guide the generation of fixes and contracts.
Such characterization is done by analyzing program state across the execution of
tests; state can be defined using user-defined query operations [74,75], and addi-
tional expressions extracted from the code [53]. Generation of program fixes and
