Satisfiability and synthesis modulo oracles

DOI10.1007/978-3-030-94583-1_13MaRDI QIDQ2152655zbMATH OpenOpenAlexFDO

Authors Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia

Publication date 8 July 2022

Full work available at URL https://arxiv.org/abs/2107.13477

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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.

Recommendations

• Refutation-based synthesis in SMT
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Counterexample guided inductive synthesis modulo theories
• Modular synthesis of sketches using models
• From program verification to program synthesis

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• A theory of formal synthesis via inductive learning
• Automated formal synthesis of provably safe digital controllers for continuous plants
• Counterexample guided inductive synthesis modulo theories
• Learning regular sets from queries and counterexamples
• Model finding for recursive functions in SMT
• SAT-Based Model Checking without Unrolling
• Scaling enumerative program synthesis via divide and conquer
• Theory and Applications of Satisfiability Testing

Cited in

(5)

• Counterexample-guided quantifier instantiation for synthesis in SMT
• Bootstrapping library-based synthesis
• Refutation-based synthesis in SMT
• Machine learning and logic: a new frontier in artificial intelligence
• Characterizations of reduction classes modulo oracle conditions

Describes a project that uses

Uses Software

• CVC4SY
• Nunchaku
• TRANSIT
• CVC4
• MiniSat

This page was built for publication: Satisfiability and synthesis modulo oracles

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2152655)