Satisfiability and Synthesis Modulo Oracles

Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 synthesis modulo oracles. In this setting, oracles may be 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 satisfiability modulo theories and oracles, 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 are able to solve problems beyond the abilities of standard SMT and synthesis solvers.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
Subtitle of host publication23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings
EditorsBernd Finkbeiner, Thomas Wies
Place of PublicationCham, Switzerland
PublisherSpringer International Publishing
Number of pages12
ISBN (Electronic)978-3-030-94583-1
ISBN (Print)978-3-030-94582-4
Publication statusPublished - 14 Jan 2022
Event23rd International Conference on Verification, Model Checking, and Abstract Interpretation - Philadelphia, United States
Duration: 16 Jan 202218 Jan 2022
Conference number: 23

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated titleVMCAI 2022
Country/TerritoryUnited States
Internet address


Dive into the research topics of 'Satisfiability and Synthesis Modulo Oracles'. Together they form a unique fingerprint.

Cite this