Program synthesis: challenges and opportunities

Journal article

Program synthesis is the mechanised 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 synthesiser generates an implementation that provably satisfies this specification. From a logical point of view, a program synthesiser 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.

Authors: Kroening, D; David, C

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Royal Society
• Journal: Philosophical Transactions A: Mathematical, Physical and Engineering Sciences
• Volume: 375
• Issue: 2104
• Pages: 1-20
• Publication date: 2017-09-04
• Acceptance date: 2017-07-13
• DOI: 10.1098/rsta.2015.0403
• EISSN: 1471-2962
• ISSN: 1364-503X