English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Given a specification $\varphi(X,Y)$ over inputs $X$ and output $Y$, definedover a background theory $\mathbb{T}$, the problem of program synthesis is todesign a program $f$ such that $Y=f(X)$ satisfies the specification $\varphi$.Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominantapproach for program synthesis where in addition to the specification$\varphi$, the end-user also specifies a grammar $L$ to aid the underlyingsynthesis engine. This paper investigates the feasibility of synthesistechniques without grammar, a sub-class defined as $\mathbb{T}$-constrainedsynthesis.  We show that $\mathbb{T}$-constrained synthesis can be reduced toDQF($\mathbb{T}$), i.e., to the problem of finding a witness of a DependencyQuantified Formula Modulo Theory. When the underlying theory is the theory ofbitvectors, the corresponding DQF(BV) problem can be further reduced toDependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBFsolving to design DQBF-based synthesizers that outperform the domain-specificprogram synthesis techniques, thereby positioning DQBF as a core representationlanguage for program synthesis. Our empirical analysis shows that$\mathbb{T}$-constrained synthesis can achieve significantly better performancethan syntax-guided approaches. Furthermore, the general-purpose DQBF solversperform on par with domain-specific synthesis techniques.

Program Synthesis as Dependency Quantified Formula Modulo Theory