# [Review] Dimensions in Program Synthesis (PPDP’10)

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

#### ML-based Methods

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