SoD-TEAM: Programming by Sketching

University Of California-Berkeley, Berkeley CA

Investigators

Abstract

0613997 Rastislav Bodik U of Cal - Berkeley TITLE Programming by Sketching Software is designed and implemented in a layered way: requirements are refined into designs, which are in turn implemented with low-level code. The implementation gap is responsible for the lack of a formal correctness connection between the layers: functionality is typically not formally specified and implementations are produced by hand rather than generated. This project proposes to bridge the implementation gap by making it easier both to write specifications and to implement the low-level code. To make the challenging problem manageable, the project focuses on the domain of scientific computing. The chief technical approach is sketching, a new software synthesis approach where the programmer develops a partial implementation --- a sketch --- and a separate specification of the desired functionality. The synthesizer then completes the sketch to behave like the specification. This exploratory project will (a) investigate how to extend the applicability of a SAT-based synthesizer to increasingly larger programs; b) develop techniques for synthesizing programs that are currently beyond the power of the SAT synthesizer; and (c) develop a robust sketching synthesizer for a class of scientific programs.