Examples are often a natural way to specify computationalstructures such as programs, queries, and sequences. Synthesizingsuch structures from example based specification has applicationsin automating end-user programming and in building intelligenttutoring systems. Synthesis from examples involves addressing twokey technical challenges: (i) design of an efficient searchalgorithm - these algorithms have been based on paradigms fromvarious communities including use of SAT/SMT solvers (formalmethods community), version space algebras (machine learningcommunity), and A*-style goal-directed heuristics (AI community).(ii) design of a user interaction model to deal with the inherentambiguity in the example based specification. In this talk, I willillustrate various algorithmic techniques and user interactionmodels by describing inductive synthesizers for varied applicationsincluding synthesis of tricky bitvector algorithms, spreadsheetmacros for automating repetitive data manipulation tasks,ruler/compass based geometry constructions, new algebra problems,sequences for mathematical intellisense, and grading of programmingproblems.
Thursday, May 03, 2012
Free and open to the public