
We introduce a model that learns to convert simple hand drawings into
graphics programs written in a subset of \LaTeX. The model combines techniques
from deep learning and program synthesis. We learn a convolutional neural
network that proposes plausible drawing primitives that explain an image. These
drawing primitives are like a trace of the set of primitive commands issued by
a graphics program. We learn a model that uses program synthesis techniques to
recover a graphics program from that trace. These programs have constructs like
variable bindings, iterative loops, or simple kinds of conditionals. With a
graphics program in hand, we can correct errors made by the deep network,
measure similarity between drawings by use of similar highlevel geometric
structures, and extrapolate drawings. Taken together these results are a step
towards agents that induce useful, humanreadable programs from perceptual
input.

We present a new approach for building sourcetosource transformations that
can run on multiple programming languages, based on a new way of representing
programs called incremental parametric syntax. We implement this approach in
Haskell in our Cubix system, and construct incremental parametric syntaxes for
C, Java, JavaScript, Lua, and Python. We demonstrate a wholeprogram
refactoring tool that runs on all of them, along with three smaller
transformations that each run on several. Our evaluation shows that (1) once a
transformation is written, little work is required to configure it for a new
language (2) transformations built this way output readable code which preserve
the structure of the original, according to participants in our human study,
and (3) our transformations can still handle language cornercases, as
validated on compiler test suites.

In this position paper, we describe our vision of the future of machine
programming through a categorical examination of three pillars of research.
Those pillars are: (i) intention, (ii) invention, and(iii) adaptation.
Intention emphasizes advancements in the humantocomputer and
computertomachinelearning interfaces. Invention emphasizes the creation or
refinement of algorithms or core hardware and software building blocks through
machine learning (ML). Adaptation emphasizes advances in the use of MLbased
constructs to autonomously evolve software.

We present a technique for static enforcement of highlevel, declarative
information flow policies. Given a program that manipulates sensitive data and
a set of declarative policies on the data, our technique automatically inserts
policyenforcing code throughout the program to make it provably secure with
respect to the policies. We achieve this through a new approach we call
typetargeted program synthesis, which enables the application of traditional
synthesis techniques in the context of global policy enforcement. The key
insight is that, given an appropriate encoding of policy compliance in a type
system, we can use type inference to decompose a global policy enforcement
problem into a series of small, local program synthesis problems that can be
solved independently.
We implement this approach in Lifty, a core DSL for datacentric
applications. Our experience using the DSL to implement three case studies
shows that (1) Lifty's centralized, declarative policy definitions make it
easier to write secure datacentric applications, and (2) the Lifty compiler is
able to efficiently synthesize all necessary policyenforcing code, including
the code required to prevent several reported realworld information leaks.

Program synthesis is a class of regression problems where one seeks a
solution, in the form of a sourcecode program, mapping the inputs to their
corresponding outputs exactly. Due to its precise and combinatorial nature,
program synthesis is commonly formulated as a constraint satisfaction problem,
where inputoutput examples are encoded as constraints and solved with a
constraint solver. A key challenge of this formulation is scalability: while
constraint solvers work well with a few wellchosen examples, a large set of
examples can incur significant overhead in both time and memory. We describe a
method to discover a subset of examples that is both small and representative:
the subset is constructed iteratively, using a neural network to predict the
probability of unchosen examples conditioned on the chosen examples in the
subset, and greedily adding the least probable example. We empirically evaluate
the representativeness of the subsets constructed by our method, and
demonstrate such subsets can significantly improve synthesis time and
stability.

The paper describes a new algorithm to generate minimal, stable, and symbolic
corrections to an input that will cause a neural network with ReLU neurons to
change its output. We argue that such a correction is a useful way to provide
feedback to a user when the neural network produces an output that is different
from a desired output. Our algorithm generates such a correction by solving a
series of linear constraint satisfaction problems. The technique is evaluated
on a neural network that has been trained to predict whether an applicant will
pay a mortgage.

In this paper, we present ReaS, a technique that combines numerical
optimization with SAT solving to synthesize unknowns in a program that involves
discrete and floating point computation. ReaS makes the program endtoend
differentiable by smoothing any Boolean expression that introduces
discontinuity such as conditionals and relaxing the Boolean unknowns so that
numerical optimization can be performed. On top of this, ReaS uses a SAT solver
to help the numerical search overcome local solutions by incrementally fixing
values to the Boolean expressions. We evaluated the approach on 5 case studies
involving hybrid systems and show that ReaS can synthesize programs that could
not be solved by previous SMT approaches.

We consider the problem of diagnosis where a set of simple observations are
used to infer a potentially complex hidden hypothesis. Finding the optimal
subset of observations is intractable in general, thus we focus on the problem
of active diagnosis, where the agent selects the next mostinformative
observation based on the results of previous observations. We show that under
the assumption of uniform observation entropy, one can build an implication
model which directly predicts the outcome of the potential next observation
conditioned on the results of past observations, and selects the observation
with the maximum entropy. This approach enjoys reduced computation complexity
by bypassing the complicated hypothesis space, and can be trained on
observation data alone, learning how to query without knowledge of the hidden
hypothesis.

Maintaining leadership in HPC requires the ability to support simulations at
large scales and fidelity. In this study, we detail one of the most significant
productivity challenges in achieving this goal, namely the increasing
proclivity to bugs, especially in the face of growing hardware and software
heterogeneity and sheer system scale. We identify key areas where timely new
research must be proactively begun to address these challenges, and create new
correctness tools that must ideally play a significant role even while ramping
up toward exacale. We close with the proposal for a twoday workshop in which
the problems identified in this report can be more broadly discussed, and
specific plans to launch these new research thrusts identified.

Recent work has proposed a promising approach to improving scalability of
program synthesis by allowing the user to supply a syntactic template that
constrains the space of potential programs. Unfortunately, creating templates
often requires nontrivial effort from the user, which impedes the usability of
the synthesizer. We present a solution to this problem in the context of
recursive transformations on algebraic datatypes. Our approach relies on
polymorphic synthesis constructs: a small but powerful extension to the
language of syntactic templates, which makes it possible to define a program
space in a concise and highly reusable manner, while at the same time retains
the scalability benefits of conventional templates. This approach enables
endusers to reuse predefined templates from a library for a wide variety of
problems with little effort. The paper also describes a novel optimization that
further improves the performance and scalability of the system. We evaluated
the approach on a set of benchmarks that most notably includes desugaring
functions for lambda calculus, which force the synthesizer to discover Church
encodings for pairs and boolean operations.

SyntaxGuided Synthesis (SyGuS) is the computational problem of finding an
implementation f that meets both a semantic constraint given by a logical
formula $\varphi$ in a background theory T, and a syntactic constraint given by
a grammar G, which specifies the allowed set of candidate implementations. Such
a synthesis problem can be formally defined in SyGuSIF, a language that is
built on top of SMTLIB.
The SyntaxGuided Synthesis Competition (SyGuSComp) is an effort to
facilitate, bring together and accelerate research and development of efficient
solvers for SyGuS by providing a platform for evaluating different synthesis
techniques on a comprehensive set of benchmarks. In this year's competition we
added a new track devoted to programming by examples. This track consisted of
two categories, one using the theory of bitvectors and one using the theory of
strings. This paper presents and analyses the results of SyGuSComp'16.

We present a novel technique for automatic program correction in MOOCs,
capable of fixing both syntactic and semantic errors without manual, problem
specific correction strategies. Given an incorrect student program, it
generates candidate programs from a distribution of likely corrections, and
checks each candidate for correctness against a test suite.
The key observation is that in MOOCs many programs share similar code
fragments, and the seq2seq neural network model, used in the naturallanguage
processing task of machine translation, can be modified and trained to recover
these fragments.
Experiment shows our scheme can correct 29% of all incorrect submissions and
outperforms state of the art approach which requires manual, problem specific
correction strategies.

We present an approach for dynamic information flow control across the
application and database. Our approach reduces the amount of policy code
required, yields formal guarantees across the application and database, works
with existing relational database implementations, and scales for realistic
applications. In this paper, we present a programming model that factors out
information flow policies from application code and database queries, a dynamic
semantics for the underlying {\lambda}^JDB core language, and proofs of
terminationinsensitive noninterference and policy compliance for the
semantics. We implement these ideas in Jacqueline, a Python web framework, and
demonstrate feasibility through three application case studies: a course
manager, a health record system, and a conference management system used to run
an academic workshop. We show that in comparison to traditional applications
with handcoded policy checks, Jacqueline applications have 1) a smaller
trusted computing base, 2) fewer lines of policy code, and 2) reasonable, often
negligible, additional overheads.

We present a method for synthesizing recursive functions that provably
satisfy a given specification in the form of a polymorphic refinement type. We
observe that such specifications are particularly suitable for program
synthesis for two reasons. First, they offer a unique combination of expressive
power and decidability, which enables automatic verificationand hence
synthesisof nontrivial programs. Second, a typebased specification for a
program can often be effectively decomposed into independent specifications for
its components, causing the synthesizer to consider fewer component
combinations and leading to a combinatorial reduction in the size of the search
space. At the core of our synthesis procedure is a new algorithm for refinement
type checking, which supports specification decomposition.
We have evaluated our prototype implementation on a large set of synthesis
problems and found that it exceeds the state of the art in terms of both
scalability and usability. The tool was able to synthesize more complex
programs than those reported in prior work (several sorting algorithms and
operations on balanced search trees), as well as most of the benchmarks tackled
by existing synthesizers, often starting from a more concise and intuitive user
input.

This paper addresses the problem of creating simplifiers for logic formulas
based on conditional term rewriting. In particular, the paper focuses on a
program synthesis application where formula simplifications have been shown to
have a significant impact. We show that by combining machine learning
techniques with constraintbased synthesis, it is possible to synthesize a
formula simplifier fully automatically from a corpus of representative
problems, making it possible to create formula simplifiers tailored to specific
problem domains. We demonstrate the benefits of our approach for synthesis
benchmarks from the SyGuS competition and automated grading.

SyntaxGuided Synthesis (SyGuS) is the computational problem of finding an
implementation f that meets both a semantic constraint given by a logical
formula $\varphi$ in a background theory T, and a syntactic constraint given by
a grammar G, which specifies the allowed set of candidate implementations. Such
a synthesis problem can be formally defined in SyGuSIF, a language that is
built on top of SMTLIB.
The SyntaxGuided Synthesis Competition (SyGuScomp) is an effort to
facilitate, bring together and accelerate research and development of efficient
solvers for SyGuS by providing a platform for evaluating different synthesis
techniques on a comprehensive set of benchmarks. In this year's competition we
added two specialized tracks: a track for conditional linear arithmetic, where
the grammar need not be specified and is implicitly assumed to be that of the
LIA logic of SMTLIB, and a track for invariant synthesis problems, with
special constructs conforming to the structure of an invariant synthesis
problem. This paper presents and analyzes the results of SyGuScomp'15.

Sketchbased synthesis, epitomized by the SKETCH tool, lets developers
synthesize software starting from a partial program, also called a sketch or
template. This paper presents JSKETCH, a tool that brings sketchbased
synthesis to Java. JSKETCH's input is a partial Java program that may include
holes, which are unknown constants, expression generators, which range over
sets of expressions, and class generators, which are partial classes. JSKETCH
then translates the synthesis problem into a SKETCH problem; this translation
is complex because SKETCH is not objectoriented. Finally, JSKETCH synthesizes
an executable Java program by interpreting the output of SKETCH.

Software synthesis is rapidly developing into an important research area with
vast potential for practical application. The SYNT Workshop on Synthesis aims
to bringing together researchers interested in synthesis to present both
ongoing and mature work on all aspects of automated synthesis and its
applications.
The second iteration of SYNT took place in Saint Petersburg, Russia, and was
colocated with the 25th International Conference on Computer Aided
Verification. The workshop included eleven presentations covering the full
scope of the emerging synthesis community, as well as a discussion lead by Swen
Jacobs on the organization of two new synthesis competitions focusing on
reactive synthesis and syntaxguided functional synthesis respectively.

We prove several decidability and undecidability results for the
satisfiability and validity problems for languages that can express solutions
to word equations with length constraints. The atomic formulas over this
language are equality over string terms (word equations), linear inequality
over the length function (length constraints), and membership in regular sets.
These questions are important in logic, program analysis, and formal
verification. Variants of these questions have been studied for many decades by
mathematicians. More recently, practical satisfiability procedures (aka SMT
solvers) for these formulas have become increasingly important in the context
of security analysis for stringmanipulating programs such as web applications.
We prove three main theorems. First, we give a new proof of undecidability
for the validity problem for the set of sentences written as a forallexists
quantifier alternation applied to positive word equations. A corollary of this
undecidability result is that this set is undecidable even with sentences with
at most two occurrences of a string variable. Second, we consider Boolean
combinations of quantifierfree formulas constructed out of word equations and
length constraints. We show that if word equations can be converted to a solved
form, a form relevant in practice, then the satisfiability problem for Boolean
combinations of word equations and length constraints is decidable. Third, we
show that the satisfiability problem for quantifierfree formulas over word
equations in regular solved form, length constraints, and the membership
predicate over regular expressions is also decidable.

We present a new method for automatically providing feedback for introductory
programming problems. In order to use this method, we need a reference
implementation of the assignment, and an error model consisting of potential
corrections to errors that students might make. Using this information, the
system automatically derives minimal corrections to student's incorrect
solutions, providing them with a quantifiable measure of exactly how incorrect
a given solution was, as well as feedback about what they did wrong.
We introduce a simple language for describing error models in terms of
correction rules, and formally define a ruledirected translation strategy that
reduces the problem of finding minimal corrections in an incorrect program to
the problem of synthesizing a correct program from a sketch. We have evaluated
our system on thousands of real student attempts obtained from 6.00 and 6.00x.
Our results show that relatively simple error models can correct on average 65%
of all incorrect submissions.

This paper presents a new approach to select events of interest to a user in
a social media setting where events are generated by the activities of the
user's friends through their mobile devices. We argue that given the unique
requirements of the social media setting, the problem is best viewed as an
inductive learning problem, where the goal is to first generalize from the
users' expressed "likes" and "dislikes" of specific events, then to produce a
program that can be manipulated by the system and distributed to the collection
devices to collect only data of interest. The key contribution of this paper is
a new algorithm that combines existing machine learning techniques with new
program synthesis technology to learn users' preferences. We show that when
compared with the more standard approaches, our new algorithm provides up to
orderofmagnitude reductions in model training time, and significantly higher
prediction accuracies for our target application. The approach also improves on
standard machine learning techniques in that it produces clear programs that
can be manipulated to optimize data collection and filtering.

Developing highperformance applications that interact with databases is a
difficult task, as developers need to understand both the details of the
language in which their applications are written in, and also the intricacies
of the relational model. One popular solution to this problem is the use of
objectrelational mapping (ORM) libraries that provide transparent access to
the database using the same language that the application is written in.
Unfortunately, using such frameworks can easily lead to applications with poor
performance because developers often end up implementing relational operations
in application code, and doing so usually does not take advantage of the
optimized implementations of relational operations, efficient query plans, or
push down of predicates that database systems provide. In this paper we present
QBS, an algorithm that automatically identifies fragments of application logic
that can be pushed into SQL queries. The QBS algorithm works by automatically
synthesizing invariants and postconditions for the original code fragment. The
postconditions and invariants are expressed using a theory of ordered relations
that allows us to reason precisely about the contents and order of the records
produced even by complex code fragments that compute joins and aggregates. The
theory is close in expressiveness to SQL, so the synthesized postconditions can
be readily translated to SQL queries. Using 40 code fragments extracted from
over 120k lines of opensource code written using the Java Hibernate ORM, we
demonstrate that our approach can convert a variety of imperative constructs
into relational specifications.