October 14, 2022
Component-based synthesis seeks to build programs using the APIs provided by a set of libraries. Often, these APIs have effects (like mutating states) which make it challenging to reason about the correctness of potential synthesis candidates. This is because changes to the global state made by effectful library procedures affect how they may be composed together. This will yield an intractably large search space that can confound typical enumerative synthesis techniques. If the nature of these effects is exposed as part of their specification, however, deductive synthesis approaches can be used to help guide the search for components.
In this talk, he will 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 and a backward search process. The forward search seeks to build larger terms given an existing context but is otherwise unaware of the actual goal. The backward search mechanism seeks terms consistent with the desired goal but is otherwise unaware of the context from which these terms must be synthesized. To further improve efficiency and scalability, they integrate a conflict-driven learning procedure into the synthesis algorithm that provides a semantic characterization of previously encountered unsuccessful search paths that are used to prune the space of possible candidates as synthesis proceeds.
They have implemented their ideas in a tool called Cobalt, and in the talk, he will demonstrate its effectiveness on several challenging synthesis problems defined over OCaml libraries equipped with effectful specifications. (Based on a recent work with Suresh Jagannathan, accepted at OOPSLA’ 22)
About Ashish Mishra
Ashish Mishra is a Postdoctoral Researcher at Purdue University working with Prof Suresh Jagannathan in the areas of Programming Languages, Program Verification and Program Synthesis.