Proving unrealizability for syntax-guided synthesis

DOI10.1007/978-3-030-25540-4_18MaRDI QIDQ6194585zbMATH OpenOpenAlexFDO

Authors Qinheping Hu, Jason Breck, John Cyphert, Loris D'Antoni, Thomas Reps

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general SyGuS instances in which the grammar describing the search space contains infinitely many programs. By encoding the synthesis problem's grammar G as a nondeterministic program P_G, we reduce the unrealizability problem to a reachability problem such that, if a standard program-analysis tool can establish that a certain assertion in P_G always holds, then the synthesis problem is unrealizable. Our method can be used to augment any existing SyGus tool so that it can establish that a successfully synthesized program q is optimal with respect to some syntactic cost -- e.g., q has the fewest possible if-then-else operators. Using known techniques, grammar G can be automatically transformed to generate exactly all programs with lower cost than q -- e.g., fewer conditional expressions. Our algorithm can then be applied to show that the resulting synthesis problem is unrealizable. We implemented the proposed technique in a tool called NOPE. NOPE can prove unrealizability for 59/134 variants of existing linear-integer-arithmetic SyGus benchmarks, whereas all existing SyGus solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them.

Recommendations

• Syntax-guided synthesis with quantitative syntactic objectives
• Overfitting in synthesis: theory and practice
• Refutation-based synthesis in SMT
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Syntax-guided termination analysis

Cited in

(2)

• Approximate bit dependency analysis to identify program synthesis problems as infeasible
• Overfitting in synthesis: theory and practice

This page was built for publication: Proving unrealizability for syntax-guided synthesis

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