Program synthesis

In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automation. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus.^[1]

The primary application of program synthesis is to relieve the programmer of the burden of writing correct, efficient code that satisfies a specification. However, program synthesis also has applications to superoptimization and inference of loop invariants.^[2]

^ Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). Program Development in Computational Logic. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.
^ (Alur, Singh & Fisman)

[1] Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). Program Development in Computational Logic. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.

[2] (Alur, Singh & Fisman)

[1]

[2]