Published: 2nd February 2016
DOI: 10.4204/EPTCS.202
ISSN: 2075-2180

EPTCS 202

Proceedings Fourth Workshop on
Synthesis
San Francisco, CA, USA, 18th July 2015

Edited by: Pavol Černý, Viktor Kuncak and Madhusudan Parthasarathy

Preface
Pavol Černý, Viktor Kuncak and Madhusudan Parthasarathy
Probabilistic Programming: Algorithms, Implementation and Synthesis
Aditya Nori
1
Programming by Examples applied to Data Manipulation
Sumit Gulwani
2
Results and Analysis of SyGuS-Comp'15
Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama
3
The Second Reactive Synthesis Competition (SYNTCOMP 2015)
Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup and Adam Walker
27
Synthesizing a Lego Forklift Controller in GR(1): A Case Study
Shahar Maoz and Jan Oliver Ringert
58
A multi-paradigm language for reactive synthesis
Ioannis Filippidis, Richard M. Murray and Gerard J. Holzmann
73
Compositional Algorithms for Succinct Safety Games
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin and Ocan Sankur
98
Specification Format for Reactive Synthesis Problems
Ayrat Khalimov
112
The complexity of approximations for epistemic synthesis (extended abstract)
Xiaowei Huang and Ron van der Meyden
120

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:

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

Aditya Nori (Microsoft Research)

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

Sumit Gulwani (Microsoft Research)

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.