Program Synthesis with Sketch Mocking

April 17, 2020
1:00
Zoom
Speaker: Nate Bragg
Host: Kathleen Fisher

Abstract

As expressed in the inaugural paper "Synthesis: Dreams => Programs" by Manna and Wildinger, program synthesis is a field dedicated to deriving programs systematically from given specifications.

State of the art synthesis algorithms treat this as a quantified boolean formula with a single exists-forall quantifier alternation, a class of problems which is challenging to solve efficiently. Improving performance in practice depends on properly formulating problems for the synthesizer.

The goal of this talk is to show how while writing code, programmers deliberately include in their programs extra information not part of the explicit specification that once extracted we can nonetheless leverage during synthesis.

We introduce Sketch Mocking, which augments the Sketch synthesis language by using this extra information to help decouple the parts of a program so that they can be synthesized in smaller pieces.

Our approach is successful at improving total performance of synthesis and verification for a certain class of problems by a factor of two to ten, and performance synthesis alone by over a factor of ten.

Zoom Link: https://tufts.zoom.us/j/9059307608

See the colloquium announcement email for the Zoom password.