SYNT 2020

Why haven't program synthesis tools been adopted into mainstream programming practice, even as synthesis techniques proliferate? Why aren't more non-coders and novice coders using synthesis to write programs? This talk dives into the process of developing a usable synthesis-backed programming tool — a Programming-By-Demonstration tool for writing web automation programs, aimed at social scientists and other non-technical domain experts. We'll discuss the lessons this project taught us about making synthesis tools work for real users and why traditional Programming By Demonstration and Programming By Example aren't always enough.

The performance of a syntax-guided synthesis algorithm is highly dependent on the provision of a good syntactic template, or grammar. Provision of such a template is often left to the user to do manually, though in the absence of such a grammar, state-of-the-art solvers will provide their own default grammar, which is dependent on the signature of the target program to be sythesized. In this work, we speculate this default grammar could be improved upon substantially. We build sets of rules, or metagrammars, for constructing grammars, and perform a gradient descent over these metagrammars aiming to find a metagrammar which solves more benchmarks and on average faster. We show that the resulting metagrammar enables CVC4 to solve 26% more benchmarks within a 300s time-out, and that metagrammars learnt from tens of benchmarks generalise to performance on 100s of benchmarks.

We describe an integration of program synthesis into UCLID5, a formal modelling and verification tool. To the best of our knowledge, the new version of UCLID5 is the only tool that supports program synthesis with bounded model checking, k‐induction, sequential program verification, and hyperproperty verification. We use the integration to generate 25 program synthesis benchmarks with simple, known solutions that are out of reach of current synthesis engines, and we release the benchmarks to the community.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains. In this work we present just-in-time synthesis (JITS) for GR(1), a novel means to execute synthesized reactive systems. Rather than constructing a controller at synthesis time, we compute next states during system execution, and only when they are required. We prove that JITS does not compromise the correctness of the synthesized system execution. We further show that the basic algorithm can be extended to enable several variants. We have implemented JITS in the Spectra synthesizer. Our evaluation, comparing JITS to existing GR(1) tools over known benchmark specifications, shows that JITS reduces (1) total synthesis time, (2) the size of the synthesis output, and (3) the loading time for system execution, all while having little to no effect on system execution performance.

This paper formulates new methods for reactive program synthesis that are fundamentally modular in nature. That helps overcome state explosion which otherwise severely limits scalability.

We present a framework to extract structured information from unstructured natural language text. We show that even in an unstructured document we can extract information as long as the information has some syntactic structure to it. We develop a framework that takes a corpus of documents and examples of entities to be extracted in very few of these documents. The framework then uses ML and program synthesis techniques to annotate the entities in the rest of the documents in the corpus. The programs synthesized by the framework are in a substring based DSL that we develop. We add the operator SubstringNearSubject which is similar to an input feature to the ML model in classical information retrieval systems. We observe improvement in performance of the entity extraction framework when we add this operator to the language. We show that developing more expressive DSLs using more features used in classical ML techniques might lead to improvement in performance. We also present our argument about how machine learning and program synthesis complement each other to make the most efficient utilization of information generated by each other.

Program synthesis traditionally entails generating programs from formal and verifiable specifications such as input-output examples, traces, or constraints. However, many real-life applications admit fuzzier specification mechanisms such as natural language descriptions or just the surrounding program context. In the machine learning community, program generation from natural language is known as semantic parsing, and while advanced, it often struggles with generating correct and executable programs. In this talk, I will describe how symbolic program synthesis and neural semantic parsing augment each other in practical applications. We'll see how natural language regularizes learning Web automation scripts from user demonstrations and how program synthesis makes question answering systems over relational databases and images more generalizable.