Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
Review
. 2017 Oct 13;375(2104):20150403.
doi: 10.1098/rsta.2015.0403.

Program synthesis: challenges and opportunities

Cristina David  1 , Daniel Kroening  2
Affiliations
Review

Program synthesis: challenges and opportunities

Cristina David et al. Philos Trans A Math Phys Eng Sci. .

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'.

Keywords: model checking; synthesis; verification.

PubMed Disclaimer

Conflict of interest statement

The authors declare that they have no competing interests.

Figures

Figure 1.
Figure 1.
Traditional workflow for using a computer to solve a problem. (Online version in colour.)
Figure 2.
Figure 2.
Program synthesis-based workflow for using a computer to solve a problem. (Online version in colour.)
Figure 3.
Figure 3.
The CEGIS loop. (Online version in colour.)
Figure 4.
Figure 4.
A program that is unsafe if there exists a candidate solution satisfying the specification for all inputs.
Figure 5.
Figure 5.
Formulae encoding the termination and safety of a single loop.
Figure 6.
Figure 6.
The language formula image (taken from [9]).
Figure 7.
Figure 7.
Formulae encoding the non-termination of a single loop.
Figure 8.
Figure 8.
Unnecessary dependency initial.
Figure 9.
Figure 9.
Unnecessary dependency refactored.
Figure 10.
Figure 10.
The CEGIS loop with solution generalization. (Online version in colour.)
Figure 11.
Figure 11.
Decision tree for increasing parameters of formula image (taken from [9]). (Online version in colour.)
Figure 12.
Figure 12.
A tricky bitvector program (taken from [9]).
Figure 13.
Figure 13.
Rules for extending an m-bit wide number to an n-bit wide one (taken from [9]).
Figure 14.
Figure 14.
Formulae encoding total correctness of a loop.
Figure 15.
Figure 15.
Filter example (taken from [6]).
See this image and copyright information in PMC

References

    1. Church A. 1962. Logic, arithmetic, automata. In Proc. Int. Congress Mathematicians, pp. 23–35. Djursholm, Sweden: Inst. Mittag-Leffler.
    1. Manna Z, Waldinger RJ. 1971. Toward automatic program synthesis. Commun. ACM 14, 151–165. ( 10.1145/362566.362568) - DOI
    1. Kraan I, Basin DA, Bundy A. 1992. Logic program synthesis via proof planning. In Proc. of LOPSTR 92, Int. Workshop on Logic Program Synthesis and Transformation, Manchester, UK, 2–3 July 1992, pp. 1–14. Berlin, Germany: Springer.
    1. Cunningham W. 1992. The wycash portfolio management system. SIGPLAN OOPS Mess 4, 29–30. ( 10.1145/157710.157715) - DOI
    1. Kruchten P, Nord RL, Ozkaya L. 2012. Technical debt: from metaphor to theory and practice. IEEE Software 29, 18–21. ( 10.1109/MS.2012.167) - DOI

LinkOut - more resources