Satisfiability and Synthesis Modulo Oracles

Elizabeth Polgreen, Andrew Reynolds, and Sanjit A. Seshia. Satisfiability and Synthesis Modulo Oracles. In Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2022.
Early technical report version available here.

Download

[pdf] 

Abstract

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms 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 oracle is eithernot available or not easy to work with? We present a framework for solving a general class of oracle-guided synthesis problems which we term <i>synthesis modulo oracles</i> (SyMO). In this setting, oracles are black boxes with a query-response interface defined by the synthesis problem. As a necessary component of this framework, we also formalize the problem of <i>satisfiability modulo theories and oracles</i> (SMTO), and present an algorithm for solving this problem.We implement a prototype solver for satisfiability and synthesis modulo oracles and demonstrate that, by using oracles that execute functions not easily modeled in SMT-constraints, such as recursive functions or oracles that incorporate compilation and execution of code, SMTO and SyMO can solve problems beyond the abilities of standard SMT and synthesis solvers.

BibTeX

@inproceedings{polgreen-vmcai22,
  author    = {Elizabeth Polgreen and Andrew Reynolds and Sanjit A. Seshia},
  title     = {Satisfiability and Synthesis Modulo Oracles},
 booktitle = {Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
 month = "January",
 year = {2022},
 abstract = {In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms 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 oracle is either
not available or not easy to work with? 
We present a framework for solving a general class of oracle-guided synthesis problems which we term {\em synthesis modulo oracles} (SyMO). In this setting, oracles are black boxes with a query-response interface defined by the synthesis problem. As a necessary component of this framework, we also formalize the problem of {\em satisfiability modulo theories and oracles} (SMTO), and present an algorithm for solving this problem.
We implement a prototype solver for satisfiability and synthesis modulo oracles and demonstrate that, by using oracles that execute functions not easily modeled in SMT-constraints, such as recursive functions or oracles that incorporate compilation and execution of code, SMTO and SyMO can solve problems beyond the abilities of standard SMT and synthesis solvers.},
  wwwnote = {Early technical report version available <a href="https://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-10.html">here</a>.}
}