Preface

The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyberphysical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in particular application domains is encouraged.

The fourth iteration of the workshop took place in San Francisco, CA, USA. It was co-located with the 27th International Conference on Computer Aided Verification. The workshop included five contributed talks and two invited talks. In addition, it featured a special session about the Syntax-Guided Synthesis Competition (SyGuS) and the SyntComp Synthesis competition.

The workshop consisted of two invited talks, five contributed talks with regular papers, and two synthesis competition reports. We thank the invited speakers, Sumit Gulwani and Aditya Nori, both of Microsoft Research. Furthermore, we thank Dana Fisman and Swen Jacobs for their presentations on the results of the Syntax-Guided Synthesis Competition (SyGuS) and the Synthesis Competition for Reactive Systems (SyntComp), respectively.

The selected papers and contributed talks have emerged from a thorough reviewing process with three to four reviews per paper. Our thanks go to the SYNT 2015 program committee:

• Colin de la Higuera, Nantes University
• Rudiger Ehlers, University of Bremen
• Bernd Finkbeiner, Saarland University
• Dana Fisman, University of Pennsylvania
• Carlo A. Furia, ETH Zurich
• Barbara Jobstmann, EPFL
• Daniel Neider, UIUC
• Doron Peled, Bar Ilan University
• Ingo Pill, TU Graz
• Ruzica Piskac, Yale
• Arjun Radhakrishna, University of Pennsylvania
• Leonid Ryzhyk, Carnegie Mellon University
• Sven Schewe, University of Liverpool
• Ute Schmid, University of Bamberg
• Johann Schumann, SGT, Inc/NASA Ames
• Rishabh Singh, Microsoft Research
• Douglas Smith, Kestrel Institute
• Armando Solar-Lezama, MIT
• Eran Yahav, Technion
• Steve Zdancewic, University of Pennsylvania

Finally, we would like to thank the organizers of CAV 2015 for their support in the organization of this workshop, as well as the NSF funded Expedition in Computer Augmented Program Engineering (ExCAPE) project for their sponsorship of the workshop.

Pavol Černý, Viktor Kuncak, Madhusudan Parthasarathy

Probabilistic Programming: Algorithms, Implementation and Synthesis

Recent years have seen a huge shift in the kind of programs that most programmers write. Programs are increasingly data driven instead of being algorithm driven. They use various forms of machine learning techniques to build models from data, for the purpose of decision making. Indeed, search engines, social networks, speech recognition, computer vision, and applications that use data from clinical trials, biological experiments, and sensors, are all examples of data driven programs.

We use the term "probabilistic programs" to refer to data driven programs that are written using higher-level abstractions. Though they span various application domains, all data driven programs have to deal with uncertainty in the data, and face similar issues in design, debugging, optimization and deployment.

In this talk, we describe connections this research area called "Probabilistic Programming" has with programming languages and software engineering --- this includes language design, static and dynamic analysis of programs, and program synthesis. We survey current state of the art and speculate on promising directions for future research.

Programming by Examples applied to Data Manipulation

Programming by Examples (PBE) involves synthesizing intended programs in an underlying domain-specific language from example based specifications (Espec). In this talk, I will formalize our notion of Espec and describe some principles behind designing appropriate domain-specific languages. A key technical challenge in PBE is to search for programs that are consistent with the Espec provided by the user. We have developed a divide-and-conquer based search paradigm that leverages deductive rules and version space algebras to achieve real time efficiency. Another technical challenge in PBE is to resolve the ambiguity that is inherent in the Espec. We use machine learning based ranking techniques to predict an intended program within a set of programs that are consistent with the Espec. We also leverage active-learning based user interaction models to help resolve ambiguity in the Espec. In this talk, I will demo few PBE technologies (FlashFill, FlashExtract, and FlashRelate) that have been developed using these principles for the domain of data manipulation. These technologies are useful for data scientists who typically spend 80% of their time cleaning data, and for 99% of those end users who do not know programming.