In this talk, I will briefly describe some recent program synthesis projects that are motivated by various reasons: enabling people with no programming background to develop utility programs, helping regular programmers automatically discover tricky/mundane details, and even discovery of new algorithms. These projects target synthesis of a variety of programs such as standard undergraduate textbook algorithms (e.g., sorting, dynamic programming), program inverses (e.g., decoders, deserializers), bit-vector manipulation routines, deobfuscators, graph algorithms, data transformers, algebraic algorithms, and mutual exclusion algorithms. Our tools today scale to synthesis of about 25 lines of code within an hour.

These projects cover various design points along three dimensions in program synthesis: functional specification, search space, and search technique.

• The functional specification is in the form of formal pre/postconditions, input-output examples, or partial/inefficient/related programs. Interactive rounds play an important role in resolving any potential under/over-specification.
• The search space is either over imperative/functional programs, or over restricted models of computation such as regular/context-free transducers, or succinct logical representations.
• The search technique has two components: constraint generation, and constraint solving.
• Constraint generation is input-based, path-based, or invariant-based.
• Constraint solving of resultant quantified formulas typically involves use of quantifier elimination techniques (such as Farkas Lemma, cover algorithms, sampling) that further enable efficient solving of quantifier-free constraints using off-the-shelf SAT/SMT solvers.