Program Synthesis

Major Groups

• 2011 Summer School on Program Synthesis with slides
• MIT Computer-Aided Programming (CAP) Group
  • web demo, open source tool Storyboard
• Automated Program Synthesis at Microsoft Research
• Program Sytnehsis at UC Berkeley
  • Try the Sketch open source synthesizer online
• VS3: Verification and Synthesis using SMT Solvers
  • Open source tool
    • - Synthesis over linear arithmetic open source (.zip)
    • - PINS: Path-based Inductive Synthesis (open source)
• Implicit Programming at EPFL
• Saint: Synthesis using Abstract Interpretation at Technion

Input Sources

From Traces/Paths

• Generating Range Fixes for Software Configuration. Xiong, Y., A. Hubaux, S. She, and K. Czarnecki. ICSE 2012.
• Automated Error Localization and Correction for. Imperative Programs. Robert Könighofer and Roderick Bloem. FMCAD 2011. [slides][project web]
• Data-driven synthesis for object-oriented frameworks, Kuat Yessenov, Zhilei Xu, and Armando Solar-Lezama. OOPSLA 2011. [slides][web demo][project web]
• Path-based Inductive Synthesis for Program Inversion. Saurabh Srivastava and Sumit Gulwani and Swarat Chaudhuri and Jeffrey S. Foster. PLDI 2011 [slides]
• Cause Clue Clauses: Error Localization Using Maximum Satisfiablity. Manu Jose and Rupak Majumdar. PLDI 2011. [Project web]
• Angelic Debugging. Satish Chandra, Emina Torlak, Shaon Barman and Ras Bodik. ICSE 2011. [Slides][Source code]
• Discovering Algorithms in Angelic Programs. S. Barman, R. Bodik, S. Chandra and E. Torlak, IBM Research Report RC25023, 2010.
• Programming with angelic nondeterminism. Rastislav Bodik, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, and Casey Rodarmor. POPL 2010. [Source code]

From Graphical Diagrams

• Synthesizing Data Structure Manipulations from Data Structure Configurations. Rishabh Singh, Armando Solar-Lezma. ESEC/FSE 2011. [open source tool Storyboard]

From Component Implementation

• Synthesizing Method Sequences for High-Coverage Testing. Suresh Thummalapenta, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Zhendong Su. OOPSLA 2011.

From Templates

• Template-based Program Verification and Program Synthesis. Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. STTT 2012.

Outputs

Method Sequences

• Data-driven synthesis for object-oriented frameworks, Kuat Yessenov, Zhilei Xu, and Armando Solar-Lezama. OOPSLA, 2011. [slides][web demo][project web]
• Synthesizing Method Sequences for High-Coverage Testing. Suresh Thummalapenta, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Zhendong Su. OOPSLA 2011.

Data Structure Manipulation

• Synthesizing Data Structure Manipulations from Data Structure Configurations. Rishabh Singh, Armando Solar-Lezma. ESEC/FSE 2011. [open source tool Storyboard]

Algorithms

• Template-based Program Verification and Program Synthesis. Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. STTT 2012.
• Path-based Inductive Synthesis for Program Inversion. Saurabh Srivastava and Sumit Gulwani and Swarat Chaudhuri and Jeffrey S. Foster [slides]

For Policies

• Program Synthesis in Administration of Higher-Order Permissions. Glenn Bruns and Michael Huth and Kumar Avijit. SACMAT 2011