@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{GRM21,
  title={Program Synthesis as Dependency Quantified Formula Modulo Theory},
  author={Golia, Priyanka and Roy, Subhajit and Meel, Kuldeep S.},
  booktitle=IJCAI,
  year={2021},
  month=aug,
  bib2html_rescat={Synthesis},
  bib2html_pubtype={Refereed Conference},
  bib2html_dl_pdf={https://arxiv.org/abs/2105.09221},
  abstract={
    Given a specification G(X, Y ) over inputs X and output Y and defined over a
    background theory T, the problem of program synthesis is to design a program
    f such that Y = f (X), satisfies the specification G. Over the past decade,
    syntax-guided synthesis (SyGuS) has emerged as a dominant approach to
    program synthesis where in addition to the specification G, the end-user
    also specifies a grammar L to aid the underlying synthesis engine. This
    paper investigates the feasibility of synthesis techniques without grammar,
    a sub-class defined as T constrained synthesis.
    We show that T-constrained synthesis can be reduced DQF(T),i.e., to the
    problem of finding a witness of a dependency quantified formula modulo
    theory. When the underlying theory is bitvectors, the corresponding DQF
    problem can be further reduced to Dependency Quantified Boolean Formulas
    (DQBF). We rely on the progress in DQBF solving to design DQBF-based
    synthesizers that outperform the domain-specific program synthesis
    techniques; thereby positioning DQBF as a core representation language for
    program synthesis. Our empirical analysis shows that T-constrained synthesis
    can achieve significantly better scalability than syntax-guided approaches.
    Furthermore, the general-purpose DQBF solvers perform on par with
    domain-specific synthesis techniques.
  },
}