Syntax-Guided Program Synthesis
Prof. Rajeev Alur, University of Pennsylvania
The classical synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on synthesis and optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. The formulation of the syntax-guided synthesis problem (SyGuS) is aimed at standardizing the core computational problem common to these proposals in a logical framework. In this talk, we first describe how a wide range of problems such as automatic synthesis of loop invariants, program optimization, program repair to defend against timing-based attacks, and learning programs from examples can be formalized as SyGuS instances. We then explain the counterexample-guided-inductive-synthesis strategy for solving the SyGuS problem, its different instantiations, and experimental evaluation over benchmarks from a variety of applications. We conclude by describing the Sharingan system that uses program synthesis to generate network classification programs at the session layer from positive and negative traffic examples. Sharingan accepts raw network traces as inputs, and reports potential patterns of the target traffic in a domain specific language designed for specifying session-layer quantitative properties. Our experiments show that Sharingan is able to correctly identify patterns from a diverse set of network traces and generates explainable outputs, while achieving accuracy comparable to state-of-the-art learning-based systems.
Evolving Program Synthesis
Dr. Asish Tiwari, Microsoft
Program Synthesis with Sketch
Prof. Armando Solar-Lezama
In this tutorial, I will show how to use the basic features of the sketch synthesis system. The talk will describe how to set up a synthesis problem by describing a space of possible programs using generators, and the different modes supported by sketch for creating specifications. The talk will also describe some of the more recent additions to the language, including the new numerical solver which allows one to solve sketches with real-valued unknowns.
Program Synthesis For Data Science
Prof. Yu Feng, Yanju Chen, UC Santa Barbara
Interactive Debugging of Concurrent Programs Under Relaxed Memory Models
Prof. Subhjit Roy, Indian Institute of Technology, Kanpur
Programming environments for sequential programs provide strong debugging support. However, concurrent programs, especially under relaxed memory models, lack powerful interactive debugging tools. In this work, we present Gambit, an interactive debugging environment that uses gdb to run a concrete debugging session on a concurrent program, while employing a symbolic execution on the program trace in the background simultaneously. The symbolic execution is analysed by a theorem prover to answer queries from the programmer on possible scenarios resulting from alternate thread interleavings or due to reorderings on other relaxed memory models, while synthesizing relevant repair suggestions.
Gambit can help programmers understand complex bug scenarios on alien environments, that is, when the program is deployed in the field under different concurrent schedulers and diverse memory models. While Gambit currently packages three memory models (PSO, TSO and SC) and provides support for constructs like fences and atomic blocks, the framework is extensible, allowing support for other memory models and programming constructs. We have evaluated Gambit on multiple programs and found that Gambit responds to the debug queries quite fast (about a second on an average across our benchmark programs).
Program Synthesis for Automated Data Transformations - Challenges in Real Life
RD Naik, Sayandeep Mitra, TCS Research
Learning to detect API Best Practice Violations
Dr. Pranav Garg, Amazon
CodeGuru Reviewer is an AWS service that provides automated code review comments. One of the recommendation categories in the Reviewer is API best practices. These recommendations are generated by several independent detectors or rules that detect violations of best practices over different APIs. In this talk, we will present our ongoing work to automatically synthesize such detectors from a few code examples that conform to or violate a given best practice. Based on the intuition that similar code changes repeated in different packages correspond to fixes of best practice violations, we obtain labeled code examples for synthesizing API best practice detectors by mining code changes from different repositories and clustering them. We will present our approach of synthesizing detectors from such code change clusters using decision tree and CNF learning and discuss preliminary results that show the promise of our approach.