Ruzica Piskac
Yale University, US
Title: From Decision Procedures to Synthesis Procedures
Abstract:
Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier, while increasing both the productivity of the programmer and the correctness of the produced code. We present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First we describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. The process of turning a decision procedure into a synthesis procedure will be illustrated using linear integer arithmetic as an example. This approach is implemented in Comfusy [1]. Comfusy is an extension to the Scala compiler and a tool for complete functional synthesis. It accepts as an input expressions with input and output variables and outputs code that computes output values as a function of input values. In addition, it also outputs the preconditions that the input variables have to satisfy in order for a
solution to exist.
However, writing a complete specification can be a tedious task, sometimes even harder than writing the code itself. To overcome this problem, ideally the user could provide a few input-output examples, and then the code should be automatically derived. We outline how to
broaden usability and applications of current software synthesis techniques.
We describe a live programming framework that allows end-users to perform transformations over strings using examples, and generate reusable stand-alone scripts. [2] Motivated by applications in automating repetitive file manipulations, we present synthesis algorithms and a language which are able to handle related tasks. This language contains operators like map, reduce, partition and split. They can be easily combined to create more complex transformers. The synthesis algorithms for those operations build upon and extend the functionality of a proprietary software Flash Fill, a state-of-the-art synthesis tool.
[1] Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter:
Complete functional synthesis. PLDI 2010: 316-329
[2] Sumit Gulwani, Mikaël Mayer, Filip Niksic, Ruzica Piskac:
StriSynth: Synthesis for Live Programming. ICSE (2) 2015: 701-704