Program synthesis aims at the automatic generation of “an executable implementation ... from a high-level logical specification of the desired input-to-output behavior.” The review article concentrates on syntax-guided synthesis. This approach to automatic program generation gives a specification of a function for the creation of a grammar that specifies additional semantic constraints--in effect the language in which the program is to be written--and a program implementing the specification.

The article uses a running example in which the grammar allows simple linear expressions and conditionals. One way to proceed is to search through increasingly complex expressions from the grammar for an implementation. The article describes how this can be done in a somewhat efficient manner. Other approaches are outlined; one particularly intriguing approach uses decision tree learning to determine the program. This is particularly transparent in the case where conditionals are required.

The article describes the research activity in the area as it is fostered through SV-COMP, “a competition of automated tools for software verification held annually in conjunction with [the European Joint Conferences on Theory and Practice of Software, ETAPS].”

As a survey, the article covers a considerable amount of ground, always in a lucid expository manner with adequate examples that illustrate the ideas. For readers interested in an introduction to the contemporary work on program synthesis or the automatic synthesis of programs, this article is highly recommended.