Author: Sumit Gulwani (Microsoft Research, Redmond, WA)

Applications of Program Synthesis

1. Discovery of New Algorithms
   – bitvector algothms
   – mutual-exclusion algorithms
2. Automated Repetitive Programming for End-Users
3. Teaching
4. General Purpose Programming Assistance
5. Synthesis of Program Inverse
   – compression/decompression
   – encryption/decryption
   – serialization/deserialization
   – insert/delete operations on data structures
   – transactional memory rollback
   – bidirectional programming
   – client-server applications

Dimension 1: User Intent

1. Logical Specification
   Example: sorting
   $ \forall k. (0 < k < n) \rightarrow (B[k-1] \leq B[k]) \quad \wedge $
   $ \forall k. \exists j. (0 \leq k < n) \rightarrow (0 \leq j < n \wedge B[j] = A[k])$
2. Natural Language
3. Input-Output Examples
   Trivial solution: switch-case on every I/O example (defense: restriction on search space)
   Interactive synthesizer: user-driven, synthesizer-driven
4. Traces
   Appropriate model for program by demonstration.
5. Programs
   Program deobfuscation, inversion, optimization.

Dimension 2: Search Space

Program Space

1. Operators
   Arithmetic + bitwise operators for bitvector programs
2. Control Structure
   Restricted to given looping template, program with bounded # of states, partial program with holes, or even loop-free programs.
   Loop-free programs: bitvector algorithms (arith+bitwise ops), text-editing programs (insert, locate, select, delete), geometrical construction (rule and compass), unbounded data type manipulation (matrix ops, set ops), API call sequences.

Challenge: # of possible programs is exponential to # of components

Grammars

• Regular expressoins
• DFAs
• NFAs
• Context-free grammars
• Regular transducers

Logics

First-order logics and its subclasses.

Dimension 3: Search Technique

Brute-force Search

Success examples: bitvector algorithms, mutual-exclusion algorithms

Version Space Algebra (VSA)

ML-based Methods

1. Probabilistic Inference
2. Genetic Programming
3. Logical Reasoning Based Techniques (SAT/SMT Solver)