Abstract
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.
As a concrete application of syntax-guided synthesis, we will describe 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.
We conclude by discussing challenges and opportunities for future research in syntax-guided program synthesis.