@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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>.}
}