Satisfiability and Synthesis Modulo Oracles

Elizabeth Polgreen; Andrew Reynolds; Sanjit A. Seshia

doi:10.1007/978-3-030-94583-1_13

Satisfiability and Synthesis Modulo Oracles

Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 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 language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation
Subtitle of host publication	23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings
Editors	Bernd Finkbeiner, Thomas Wies
Place of Publication	Cham, Switzerland
Publisher	Springer International Publishing
Pages	263-284
Number of pages	12
ISBN (Electronic)	978-3-030-94583-1
ISBN (Print)	978-3-030-94582-4
DOIs	https://doi.org/10.1007/978-3-030-94583-1_13
Publication status	Published - 14 Jan 2022
Event	23rd International Conference on Verification, Model Checking, and Abstract Interpretation - Philadelphia, United States Duration: 16 Jan 2022 → 18 Jan 2022 Conference number: 23 https://popl22.sigplan.org/home/VMCAI-2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	13182
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	23rd International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated title	VMCAI 2022
Country/Territory	United States
City	Philadelphia
Period	16/01/22 → 18/01/22
Internet address	https://popl22.sigplan.org/home/VMCAI-2022

Access to Document

10.1007/978-3-030-94583-1_13Licence: All Rights Reserved

Satisfiability and Synthesis_POLGREEN_DOA12102021_AFVAccepted author manuscript, 785 KBLicence: All Rights Reserved

https://link.springer.com/chapter/10.1007/978-3-030-94583-1_13Licence: All Rights Reserved

Cite this

Polgreen, E., Reynolds, A., & Seshia, S. A. (2022). Satisfiability and Synthesis Modulo Oracles. In B. Finkbeiner, & T. Wies (Eds.), Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings (pp. 263-284). (Lecture Notes in Computer Science; Vol. 13182). Springer International Publishing. https://doi.org/10.1007/978-3-030-94583-1_13

Polgreen, Elizabeth ; Reynolds, Andrew ; Seshia, Sanjit A. / Satisfiability and Synthesis Modulo Oracles. Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings. editor / Bernd Finkbeiner ; Thomas Wies. Cham, Switzerland : Springer International Publishing, 2022. pp. 263-284 (Lecture Notes in Computer Science).

@inproceedings{2c35143cdb85487e8e677b8ea60a3f61,

title = "Satisfiability and Synthesis Modulo Oracles",

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 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.",

author = "Elizabeth Polgreen and Andrew Reynolds and Seshia, {Sanjit A.}",

note = "Funding Information: Acknowledgments. We thank Susmit Jha, Michael O{\textquoteright}Boyle, Federico Mora, Adwait Godbole, Yatin Manerkar and Sebastian Junges for their feedback on earlier versions of this paper. This work was supported in part by NSF grants CNS-1739816 and CCF-1837132, by the DARPA LOGiCS project under contract FA8750-20-C-0156, by the iCyPhy center, and by gifts from Intel, Amazon, and Microsoft. Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022 ; Conference date: 16-01-2022 Through 18-01-2022",

year = "2022",

month = jan,

day = "14",

doi = "10.1007/978-3-030-94583-1_13",

language = "English",

isbn = "978-3-030-94582-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing",

pages = "263--284",

editor = "Bernd Finkbeiner and Thomas Wies",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

url = "https://popl22.sigplan.org/home/VMCAI-2022",

}

Polgreen, E, Reynolds, A & Seshia, SA 2022, Satisfiability and Synthesis Modulo Oracles. in B Finkbeiner & T Wies (eds), Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13182, Springer International Publishing, Cham, Switzerland, pp. 263-284, 23rd International Conference on Verification, Model Checking, and Abstract Interpretation, Philadelphia, Pennsylvania, United States, 16/01/22. https://doi.org/10.1007/978-3-030-94583-1_13

Satisfiability and Synthesis Modulo Oracles. / Polgreen, Elizabeth; Reynolds, Andrew; Seshia, Sanjit A.

Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings. ed. / Bernd Finkbeiner; Thomas Wies. Cham, Switzerland : Springer International Publishing, 2022. p. 263-284 (Lecture Notes in Computer Science; Vol. 13182).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Satisfiability and Synthesis Modulo Oracles

AU - Polgreen, Elizabeth

AU - Reynolds, Andrew

AU - Seshia, Sanjit A.

N1 - Conference code: 23

PY - 2022/1/14

Y1 - 2022/1/14

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-94583-1_13

DO - 10.1007/978-3-030-94583-1_13

M3 - Conference contribution

SN - 978-3-030-94582-4

T3 - Lecture Notes in Computer Science

SP - 263

EP - 284

BT - Verification, Model Checking, and Abstract Interpretation

A2 - Finkbeiner, Bernd

A2 - Wies, Thomas

PB - Springer International Publishing

CY - Cham, Switzerland

T2 - 23rd International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 16 January 2022 through 18 January 2022

ER -

Polgreen E, Reynolds A, Seshia SA. Satisfiability and Synthesis Modulo Oracles. In Finkbeiner B, Wies T, editors, Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings. Cham, Switzerland: Springer International Publishing. 2022. p. 263-284. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-94583-1_13

Satisfiability and Synthesis Modulo Oracles

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this