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. Feb 09 2021 13.00 - 14.00 Lab Lunch: 9 February 2021 - Elizabeth Polgreen Speaker: Elizabeth Polgreen Blackboard Collaborate Invitation Only
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. Feb 09 2021 13.00 - 14.00 Lab Lunch: 9 February 2021 - Elizabeth Polgreen Speaker: Elizabeth Polgreen Blackboard Collaborate Invitation Only
Feb 09 2021 13.00 - 14.00 Lab Lunch: 9 February 2021 - Elizabeth Polgreen Speaker: Elizabeth Polgreen
