Lab Lunch: 9 February 2021 - Elizabeth Polgreen

Title: Synthesis Modulo Oracles  

Abstract:

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box SMT oracle is either not available or not easy to work with?

In this talk, I’ll present a framework for solving a general class of oracle-guided synthesis problems, which we term “synthesis modulo oracles”.  In this setting, oracles may be black boxes with a query-response interface defined by the synthesis problem. As a necessary part of this framework, I will also formalise the problem of satisfiability modulo oracles and present an algorithm for solving this problem.

This is work-in-progress, and I’ll also discuss preliminary results on the application of this framework.

Dr. Elizabeth Polgreen is a Lecturer in Programming Languages for Trustwor thy Systems.