Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Modular Synthesis in Sketch

PI: Solar-Lezama (MIT)

In the programming approach advocated by the Sketch system, a programmer writes a partial program with incomplete details, and the synthesizer fills in the missing details using user-specified assertions as the correctness specification. We are exploring different ways of enhancing the usability and scalability of Sketch. Recent work focuses on the problem of modular synthesis by relying on user-provided models of complex functions. The approach looks at how the user can write simple models to abstract complex functionality and how using such models can make computationally demanding synthesis problems tractable. Their research shows that introducing models can potentially interfere with the counterexample-guided- inductive-synthesis algorithm used by Sketch, and they propose a solution to overcome this challenge. Showing that an implementation is represented by a model is also tricky because it requires an extra quantifier to show that there exists a behavior of the model that matches the behavior of the implementation on a given input. However, their work shows how a few simple restrictions on the model can allow the quantifier to be eliminated without placing additional stress on the solver [SSZKS14].


ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996