---
abstract: |
    We consider the problem of automatically establishing that a given syntax-guided-synthesis () problem is *unrealizable* (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general 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 existing tools so that they 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 transformed to generate the set of all programs with lower costs 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 . can prove unrealizability for /variants of existing linear-integer-arithmetic benchmarks, whereas all existing solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them.
author:
- |
    Qinheping Hu$^1$, Jason Breck$^1$, John Cyphert$^1$,\
    Loris D'Antoni$^1$, Thomas Reps$^{1,2}$
bibliography:
- 'ref.bib'
title: |
    Proving Unrealizability\
    for Syntax-Guided Synthesis
---



{'source': 'arXiv_out/1905'}