SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Tue 6 Dec 2022 15:30 - 16:00 at AMRF Auditorium - Invariant and Program Synthesis Chair(s): Subhajit Roy

Constraint-based program synthesis technology has been widely used in numerous settings. However, synthesizing programs that use libraries remains a major challenge. To handle complex or black-box libraries, the state of the art is to provide carefully crafted mocks or models to the synthesizer, requiring extra manual work. We address this challenge by proposing Toshokan, a new synthesis framework as an alternative approach in which library-using programs can be generated without any user-provided artifacts at the cost of moderate performance overhead. The framework extends the classic counter-example-guided synthesis framework with a bootstrapping, log-based library model. The model collects input-output samples from running failed candidate programs on witness inputs. We prove that the framework is sound when sound, bounded verification could be achieved, and also complete if the underlying synthesizer and verifier promise to produce minimal outputs. We implement and incorporate the framework to JSketch, a Java sketching tool. Experiments show that Toshokan can successfully synthesize programs that use a wide variety of libraries, ranging from mathematical functions to data structures. Comparing to state-of-the-art synthesis algorithms which use mocks or models, Toshokan reduces up to 159 lines of code of required manual inputs, at the cost of less than 40 second of performance overheads.

Tue 6 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
Invariant and Program SynthesisSAS at AMRF Auditorium
Chair(s): Subhajit Roy IIT Kanpur
15:30
30m
Talk
Bootstrapping Library-Based Synthesis
SAS
Kangjing Huang Purdue University, USA, Xiaokang Qiu Purdue University, USA
16:00
30m
Talk
Automated Synthesis of Asynchronizations
SAS
Sidi Mohamed Beillahi University of Toronto, Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea Ecole Polytechnique / LIX / CNRS, Shuvendu K. Lahiri Microsoft Research
16:30
30m
Talk
Solving Invariant Generation for Unsolvable Loops
SAS