Techniques and Applications of Constraint-based Synthesis, Armando Solar-Lezama

This talk will describe how constraint-based synthesis can provide a unifying framework to attack problems as diverse as program optimization, automated grading, and the production of verified code. The talk will present an overview of constraint-based synthesis technology and its implementation in the Sketch synthesis platform, and it will show how this technology can be applied to each of the aforementioned domains. For program optimization, synthesis allows us to raise the level of abstraction of a program, making it possible to apply aggressive optimizations that can even change the algorithmic complexity of a piece of code. In automated grading, synthesis allows us to improve upon the traditional method of grading programs based on a test suite by allowing us to determine the set of modifications needed to make the program correct. Finally, synthesis can aid the development of verified code by deriving code that is easier to prove correct.

Видео Techniques and Applications of Constraint-based Synthesis, Armando Solar-Lezama канала ETH WSCR