CS welcomes Professor Rajeev Alur, Zisman Family Professor from the Department of Computer and Information Science at the University of Pennsylvania for its last Shutterstock Distinguished Lecture Series of 2018. All are welcome to join us in New CS, Room 120 at 2:30p.
Syntax-Guided Program Syntehsis
Abstract: The goal of program synthesis is to allow programmers to specify the desired computation in intuitive ways without having to write traditional code. 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 discussing how program synthesis and machine learning can play mutually beneficial roles to transform the way we build software.