Author: Sumit Gulwani (Microsoft Research, Redmond, WA)
Applications of Program Synthesis
- Discovery of New Algorithms
– bitvector algothms
– mutual-exclusion algorithms - Automated Repetitive Programming for End-Users
- Teaching
- General Purpose Programming Assistance
- 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
- 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])$ - Natural Language
- Input-Output Examples
Trivial solution: switch-case on every I/O example (defense: restriction on search space)
Interactive synthesizer: user-driven, synthesizer-driven - Traces
Appropriate model for program by demonstration. - Programs
Program deobfuscation, inversion, optimization.
Dimension 2: Search Space
Program Space
- Operators
Arithmetic + bitwise operators for bitvector programs - 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
- Probabilistic Inference
- Genetic Programming
- Logical Reasoning Based Techniques (SAT/SMT Solver)