ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Sun 15 Nov 2020 22:00 - 22:20 at OOPSLA/ECOOP - S-2
Sun 15 Nov 2020 10:00 - 10:20 at OOPSLA/ECOOP - S-2

Program synthesis promises to help software developers with everyday tasks by generating code snippets automatically from input-output examples and other high-level specifications. The conventional wisdom is that a synthesizer must always satisfy the specification exactly. We conjecture that this all-or-nothing paradigm stands in the way of adopting program synthesis as a developer tool: in practice, the user-written specification often contains errors or is simply too hard for the synthesizer to solve within a reasonable time; in these cases, the user is left with a single over-fitted result or, more often then not, no result at all. In this paper we propose a new program synthesis paradigm we call \emph{best-effort program synthesis}, where the synthesizer returns a ranked list of partially-valid results, i.e., programs that satisfy some part of the specification.

To support this paradigm, we develop \emph{best-effort enumeration}, a new synthesis algorithm that extends a popular program enumeration technique with the ability to accumulate and return multiple partially-valid results with minimal overhead. We implement this algorithm in a tool called Bester, and evaluate it on $79$ synthesis benchmarks from the literature. Contrary to the conventional wisdom, our evaluation shows that Bester returns useful results even when the specification is flawed or too hard: i) for all benchmarks with an error in the specification, the top three Bester results contain the correct solution, and ii) for most hard benchmarks, the top three results contain non-trivial \emph{fragments} of the correct solution. We also performed a small user study, which confirms our intuition that partially-valid results are useful: the study shows that programmers use the output of the synthesizer for comprehension and often incorporate it into their solutions.

Sun 15 Nov
Times are displayed in time zone: (GMT-05:00) Central Time (US & Canada) change

09:00 - 10:20: S-2Research Papers at OOPSLA/ECOOP +12h
09:00 - 09:20
Talk
Research Papers
Matías ToroUniversity of Chile, Éric TanterUniversity of Chile
DOI
09:20 - 09:40
Talk
Research Papers
Lukas DiekmannKing's College London, Laurence TrattKing's College London
Pre-print
09:40 - 10:00
Talk
Research Papers
Abel NietoAarhus University, Marianna RapoportUniversity of Waterloo, Gregor RichardsUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Pre-print
10:00 - 10:20
Talk
Research Papers
Hila PelegUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego
21:00 - 22:20: S-2Research Papers at OOPSLA/ECOOP
21:00 - 21:20
Talk
Research Papers
Matías ToroUniversity of Chile, Éric TanterUniversity of Chile
DOI
21:20 - 21:40
Talk
Research Papers
Lukas DiekmannKing's College London, Laurence TrattKing's College London
Pre-print
21:40 - 22:00
Talk
Research Papers
Abel NietoAarhus University, Marianna RapoportUniversity of Waterloo, Gregor RichardsUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Pre-print
22:00 - 22:20
Talk
Research Papers
Hila PelegUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego