Program sketching
By Armando Solar-Lezama. 2012
269 citations recorded by the source corpus.
Sketching is a synthesis methodology that aims to bridge the gap between a programmer’s high-level insights about a problem and the computer’s ability to manage low-level details. In sketching, the programmer uses a partial program, a sketch, to describe the desired implementation strategy, and leaves the low-level details of the implementation to an automated synthesis procedure. In order to generate an implementation from the programmer provided sketch, the synthesizer uses counterexample-guided inductive synthesis (CEGIS). Inductive synthesis refers to the process of generating candidate implementations from concrete examples of correct or incorrect behavior. CEGIS combines a SAT-based inductive synthesizer with an automated validation procedure, a bounded model-checker, that checks whether the candidate implementation produced by inductive synthesis is indeed correct and to produce new counterexamples. The result is a synthesis procedure that is able to handle complex problems from a variety of domains including ciphers, scientific programs, and even concurrent data-structures.
Subfields: Computational Theory and Mathematics, Hardware and Architecture
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computational Theory and Mathematics
- Angelika Kimmig
- Luc De Raedt
- Thomas Demeester
- Pavol Bielik
- Martin T. Vechev
- Veselin Raychev
- Sebastijan Dumancic
- Robin Manhaeve
In Hardware and Architecture
- Thomas Demeester
- Pavol Bielik
- Martin T. Vechev
- Luc De Raedt
- Veselin Raychev
- Angelika Kimmig
- Sebastijan Dumancic
- Robin Manhaeve
Citations in the corpus
- DeepProbLog: Neural Probabilistic Logic Programming (2018, positive): “We follow the program sketching [25] setting of differentiable Forth (∂4) [8], where holes in given programs need to be filled by neural networks trained on input-output examples for the entire program.”
- Probabilistic model for code with decision trees (2016, background): “Program synthesis A common challenge for many existing program synthesis techniques [5, 14, 30, 31] is scalability: it is still difficult to scale these approaches to the task of synthesizing large, practical programs.”