- author = "Cristina David and Daniel Kroening",
- title = "Program synthesis: challenges and opportunities",
- journal = "Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences",
- year = "2017",
- volume = "375",
- number = "2104",
- month = "13 " # oct,
- note = "Discussion meeting issue ``Verified trustworthy software systems'' organised and edited by Philippa Gardner, Mike Gordon, Greg Morrisett, Peter O'Hearn and Fred Schneider",
- keywords = "genetic algorithms, genetic programming, verification, model checking, synthesis, software",
- ISSN = "1364-503X",
- publisher = "Royal Society",
-
DOI = "
doi:10.1098/rsta.2015.0403",
- size = "20 pages",
-
abstract = "Program synthesis is the mechanized construction of
software, dubbed self-writing code. Synthesis tools
relieve the programmer from thinking about how the
problem is to be solved; instead, the programmer only
provides a description of what is to be achieved. Given
a specification of what the program should do, the
synthesizer generates an implementation that provably
satisfies this specification. From a logical point of
view, a program synthesizer is a solver for
second-order existential logic. Owing to the
expressiveness of second-order logic, program synthesis
has an extremely broad range of applications. We survey
some of these applications as well as recent trends in
the algorithms that solve the program synthesis
problem. In particular, we focus on an approach that
has raised the profile of program synthesis and ushered
in a generation of new synthesis tools, namely
counter-example-guided inductive synthesis (CEGIS). We
provide a description of the CEGIS architecture,
followed by recent algorithmic improvements. We
conjecture that the capacity of program synthesis
engines will see further step change, in a manner that
is transparent to the applications, which will open up
an even broader range of use-cases.
This article is part of the themed issue Verified trustworthy software systems.",
- notes = "PubMed:28871052",
