אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

Recent years have seen great progress in automated synthesis techniques that can automatically generate code based on some intent expressed by the user, but communicating this intent remains a major challenge. When the expressed intent is coarse-grained (for example, restriction on the expected type of an expression), the synthesizer often produces a long list of results for the user to choose from, shifting the heavy-lifting to the user. An alternative approach is programming by example (PBE), where the user leverages examples to interactively and iteratively refine the intent. Existing program synthesis tools are usually designed around the synthesizer and its internals. However, these are tools intended for users, who are the ones who must specify (and respecify) the specifications. Synthesis tools are often designed either with no particular group of users in mind, or with the purpose of generating code for users who cannot write and read it. We suggest instead designing synthesis tools specifically for programmers. This allows making assumptions on both the input the user can generate and the output they can consume. Concepts that are part of the programmer's life such as code review and unit tests can be levereged. The common sense of making generalizations can be aided by the user. But this approach also brings with it restrictions for the synthesizer, which pose new design challenges: examples, a common tool, are not expressive enough for programmers, who can observe the generated program and refine the intent by directly relating to parts of the generated program. Additionally, can the users correctly judge when the program is correct? We suggested a new Granular Interaction Model (GIM) and performed a controlled user study to assess its effectiveness. In addition, we modeled the interaction of the user with a synthesizer, formalizing the refinement of specification by the user and the respective reduction of the candidate program space. This model allowed us to present two conditions for termination of a synthesis session, one hinging only on the properties of the available partial specifications, and the other also on the behavior of the user. Finally, we showed conditions for realizability of the user's intent, and limitations of backtracking when it is apparent a session will fail.