EdSketch: execution-driven sketching for Java

Abstract

Sketching is a relatively recent approach to program synthesis, which has shown much promise. The key idea in sketching is to allow users to write partial programs that have ''holes'' and provide test harnesses or reference implementations, and let synthesis tools create program fragments that fill the holes such that the resulting complete program has the desired functionality. Traditional solutions to the sketching problem perform a translation to SAT and employ CEGIS. While effective for a range of programs, when applied to real applications, such translation-based approaches have a key limitation: they require either translating all relevant libraries that are invoked directly or indirectly by the given sketch -- which can lead to impractical SAT problems -- or creating models of those libraries -- which can require much manual effort.