About DryadSynth
DryadSynth is designed to automatically generate programs that satisfy both semantic specifications and user–defined syntactic constraints. By combining the strengths of enumerative and deductive techniques, DryadSynth employs a divide-and-conquer strategy that:
- Splits complex synthesis problems into manageable subproblems: Using innovative fixed-height enumeration and tailored deductive rules, the engine gradually builds up solutions.
- Supports concurrent synthesis: Its concurrent framework (see our string sub-solver "Synthphonia") coordinates asynchronous deduction and enumeration to overcome exponential search spaces.
- Is versatile across multiple domains: DryadSynth effectively supports synthesis for conditional linear integer arithmetic (CLIA), bit-vectors, and string transformations.
Based on our research published at PLDI 2020, POPL 2024, and PLDI 2025 (Conditional Accepted) , DryadSynth represents a significant step forward in scaling synthesis to problems previously deemed unsolvable.
Features
Hybrid Synthesis Approach
Combines enumerative search with deductive synthesis to explore program spaces efficiently.
Cooperative Divide-and-Conquer
Uses novel strategies to break down synthesis tasks into subproblems that can be solved independently and later recombined.
Concurrent Synthesis Engine
Integrates asynchronous deduction with a versatile enumerator (as seen in our string synthesis module, Synthphonia) for faster convergence.
Domain Versatility
Supports multiple synthesis tracks including CLIA, bit-vectors, and string transformations.
Lightweight and Extensible
Implemented in approximately 11K lines of Java leveraging the power of Z3, DryadSynth is both easy to understand and extend.
Open Source & MIT Licensed
Freely available for both research and commercial applications.
Documentation
DryadSynth is published on crates.io, the Rust package registry. Explore our packages:
- dryadsynth – Main synthesizer package
- dryadsynth-bv – Bit-vector solver package
- synthphonia-rs – String transformation solver
- simple-rc-async – Supporting library for concurrent synthesis
For further details on installation, usage, and design, please refer to ourREADME.
Publications
Reconciling Enumerative and Deductive Program Synthesis
Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, Yanjun Wang.
In Proc. 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '20).
Enhanced Enumeration Techniques for Syntax-Guided Synthesis
Yuantian Ding, Xiaokang Qiu.
In Proc. 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '24).
A Concurrent Approach to String Transformation Synthesis
Yuantian Ding, Xiaokang Qiu.
Conditional Accepted at 46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '25).
Purdue CAP Team
DryadSynth is developed by the Purdue Computer-Aided Programming (CAP) research group, focusing on program synthesis, verification, and automated reasoning.
