Themen des Seminars “Program Synthesis”

Artur Andrzejak, Lutz Büch

Sommersemester 2015, Institut für Informatik, Universität Heidelberg

Link zur Webseite: http://pvs.ifi.uni-heidelberg.de/teaching/ss2015/s-program-synthesis/

Teilnehmer

Teilnehmer

A. General Program Synthesis, Genetic Programming

A1 Survey Program Transformation

A2 Generation of Specifications

A3 Program Repair

A4 Optimisation

A5 Optimising of Compiler Optimisation

B. Programming by Example / by Demonstration

B1 Introduction to Programming by Example

B2 LaSy, Test-Driven Synthesis

B3 PowerPoint FlashFormat: Repetitive Formatting by Example

B4 FlashExtract: Data Extraction by Example

B5 FlashRelate: Table Structuring by Example

B6 Karma: Data Integration by Example

B7 DataPlay: Interactive Query Synthesis

B8 TableProg: Table transformation by Example

B9 Excel FlashFill I: String transformation by Example

B10 Excel FlashFill II: Numerical String Transformation by Example

General literature

• Google testing blog - April 01, 2014 -  The *Real* Test Driven Development

A. General Program Synthesis, Genetic Programming

A1 Survey Program Transformation

• Presenting the variants of Program Transformation
• Sec. 1-4
• Sources:

• Visser, Eelco. "A survey of rewriting strategies in program transformation systems." Electronic Notes in Theoretical Computer Science 57 (2001): 109-143. (link)
• Eelco Visser, Arie van Deursen http://www.program-transformation.org/

A2 Generation of Specifications

• Daikon: Dynamic invariant detection
• Static checking

• ESC/Java static checker

• Dynamic analysis
• Static analysis
• Source:

• Nimmer, Jeremy W., and Michael D. Ernst. "Automatic generation of program specifications." ACM SIGSOFT Software Engineering Notes. Vol. 27. No. 4. ACM, 2002. (link)

A3 Program Repair

• Transformation from non-functional to functional software
• Genetic programming

• Representation
• Selection
• Mutation
• Crossover
• Fitness Function

• Repair minimization
• Presentation of examples
• Evaluation
• Sources:

• Le Goues, Claire, et al. "GenProg: A generic method for automatic software repair." Software Engineering, IEEE Transactions on 38.1 (2012): 54-72. (link)
• Le Goues, Claire, et al. "A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each." Software Engineering (ICSE), 2012 34th International Conference on. IEEE, 2012. (link)

A4 Optimisation

• Transformation with performance objective
• Pareto Program Surface
• Functional vs non-functional properties
• Genetic programming

• Representation
• Selection
• Mutation
• Crossover
• Fitness Function

• Application: Bowtie2
• Sources:

• Harman, Mark, et al. "The GISMOE challenge: Constructing the pareto program surface using genetic programming to find better programs (keynote paper)." Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering. ACM, 2012. (link)
• Langdon, William B., and Mark Harman. "Optimising existing software with genetic programming." IEEE Transactions on Evolutionary Computation 99 (2013). (link)

A5 Optimising of Compiler Optimisation

• Selection of Compiler Optimisation options for compiling a given program
• Genetic programming

• Representation
• Selection
• Mutation
• Crossover
• Fitness Function

• Evaluation
• Source:

• Lin, San-Chih, Chi-Kuang Chang, and Nai-Wei Lin. "Automatic selection of GCC optimization options using a gene weighted genetic algorithm." Computer Systems Architecture Conference, 2008. ACSAC 2008. 13th Asia-Pacific. IEEE, 2008. (link)

B. Programming by Example / by Demonstration

B1 Introduction to Programming by Example

• Dimensions in Program Synthesis

• Expression of user intent, Interaction models
• Search space
• Search technique

• Presentation of applications, techniques
• Sources:

• Gulwani, Sumit. "Dimensions in program synthesis." Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming. ACM, 2010. (link)
• Gulwani, Sumit. "Synthesis from examples: Interaction models and algorithms." Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2012 14th International Symposium on. IEEE, 2012. (link)

B2 LaSy, Test-Driven Synthesis

• LaSy language

• search space definition
• context-free grammar

• Test-driven Synthesis

• specification
• Generation: DSL-based Synthesis

• Presentation of examples
• Source:

• Perelman, D., Gulwani, S., Grossman, D., & Provost, P. (2014, June). “Test-driven synthesis.” In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (p. 43). ACM. (link)

B3 PowerPoint FlashFormat: Repetitive Formatting by Example

• least general generalization
• FlashFormat DSL
• Synthesis algorithm
• [StyleSnap not necessarily]
• Sources:

• Raza, Mohammad, Sumit Gulwani, and Natasa Milic-Frayling. "Programming by example using least general generalizations." Twenty-Eighth AAAI Conference on Artificial Intelligence. 2014. (link)
• Edge, D., Gulwani, S., Milic-Frayling, N., Raza, M., Saputra, R. A., Wang, C., & Yatani, K. “Mixed-Initiative Approaches to Global Editing in Slideware.” CHI Conference on Human Factors in Information Systems, 2015. (link)

B4 FlashExtract: Data Extraction by Example

• Interaction model
• abstract DSL, definition of Data Extraction DSLs
• presentation of examples
• modular synthesis algorithms
• Source:

• Le, Vu, and Sumit Gulwani. "FlashExtract: A framework for data extraction by examples." Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2014. (link)

B5 FlashRelate: Table Structuring by Example

• DSL Flare
• cell constraints
• spatial constraints
• synthesis algorithm FlashRelate
• Source:

• Barowy, Daniel W., et al. "FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples." Microsoft Research Technical Report, 2014. (link)

B6 Karma: Data Integration by Example

• specification by user
• types of constraints
• Plan tree
• Monotonically decreasing property
• Source:

• Tuchinda, Rattapoom, Pedro Szekely, and Craig A. Knoblock. "Building data integration queries by demonstration." Proceedings of the 12th international conference on Intelligent user interfaces. ACM, 2007. (link)

B7 DataPlay: Interactive Query Synthesis

• Quantified queries
• query tree

• data tree
• constraints

• Interaction model
• Source:

• Abouzied, Azza, Joseph Hellerstein, and Avi Silberschatz. "DataPlay: interactive tweaking and example-driven correction of graphical database queries." Proceedings of the 25th annual ACM symposium on User interface software and technology. ACM, 2012. (link)

B8 TableProg: Table transformation by Example

• table programs DSL TableProg
• Synthesis algorithm ProgFromEx
• Presentation of examples / test cases
• Source:

• Harris, William R., and Sumit Gulwani. "Spreadsheet table transformations from examples." ACM SIGPLAN Notices. Vol. 46. No. 6. ACM, 2011. (link)

B9 Excel FlashFill I: String transformation by Example

• string transformation DSL
• search space presentation
• conditionals, partition, classifiers
• ranking
• presentation of examples
• Sources:

• Gulwani, Sumit. "Automating string processing in spreadsheets using input-output examples." ACM SIGPLAN Notices. Vol. 46. No. 1. ACM, 2011. (link)
• Gulwani, Sumit, William R. Harris, and Rishabh Singh. "Spreadsheet data manipulation using examples." Communications of the ACM 55.8 (2012): 97-105. (link)

B10 Excel FlashFill II: Numerical String Transformation by Example

• number transformation DSL
• combination language with string transformation
• search space presentation
• ranking
• presentation of examples
• Source:

• Singh, Rishabh, and Sumit Gulwani. "Synthesizing number transformations from input-output examples." Computer Aided Verification. Springer Berlin Heidelberg, 2012. (link)