Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 11:30 - 12:00 at Lecture Theatre 2 - Synthesis I Chair(s): Hakjoo Oh

Component-based synthesis seeks to build programs using the APIs
provided by a set of libraries. Oftentimes, these APIs have
effects, which make it challenging to reason about the correctness
of potential synthesis candidates. This is because changes to
global state made by effectful library procedures affect how they
may be composed together, yielding an intractably large search space
that can confound typical enumerative synthesis techniques. If the
nature of these effects are exposed as part of their specification,
however, deductive synthesis approaches can be used to help guide
the search for components. In this paper, we present a new
specification-guided synthesis procedure that uses Hoare-style pre-
and post-conditions to express fine-grained effects of potential
library component candidates to drive a bi-directional synthesis
search strategy. The procedure alternates between a forward search
process that seeks to build larger terms given an existing context
but which is otherwise unaware of the actual goal, alongside a
backward search mechanism that seeks terms consistent with the
desired goal but which is otherwise unaware of the context from
which these terms must be synthesized. To further improve
efficiency and scalability, we integrate a conflict-driven learning
procedure into the synthesis algorithm that provides a semantic
characterization of previously encountered unsuccessful search paths
that is used to prune the space of possible candidates as synthesis
proceeds. We have implemented our ideas in a tool called \name\ and
demonstrate its effectiveness on a number of challenging synthesis
problems defined over OCaml libraries equipped with effectful

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Synthesis IOOPSLA at Lecture Theatre 2
Chair(s): Hakjoo Oh Korea University
Research paper
Complexity-guided container replacement synthesisDistinguished Paper
Chengpeng Wang Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Wensheng Tang Hong Kong University of Science and Technology, Qingkai Shi Ant Group, Charles Zhang Hong Kong University of Science and Technology
Katara: Synthesizing CRDTs with Verified Lifting
Shadaj Laddad University of California at Berkeley, Conor Power University of California at Berkeley, Mae Milano University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein University of California at Berkeley
Specification-Guided Component-Based Synthesis from Effectful Libraries
Ashish Mishra Purdue University, Suresh Jagannathan Purdue University