---
title: "Syntax-Guided Synthesis — paper by Alur et al. (2013)"
description: "The authors define a single abstract problem, syntax-guided synthesis (SyGuS), built from logics and… 27 references, cited by 29 papers here."
authors: ["Rajeev Alur", "Rastislav Bodik", "Garvit Juniwal", "Milo M. K. Martin", "Mukund Raghothaman", "Sanjit A. Seshia", "Rishabh Singh", "Armando Solar-Lezama", "Emina Torlak", "Abhishek Udupa"]
year: 2013
venue: "FMCAD 2013"
source: "https://www.cis.upenn.edu/~alur/SyGuS13.pdf"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/alur-2013-syntax-guided-synthesis/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/alur-2013-syntax-guided-synthesis/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2013](https://md.research.elamur.ai/free/en/papers/2013/) / Syntax-Guided Synthesis

# Syntax-Guided Synthesis

**Authors:** Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, [Sanjit A. Seshia](https://md.research.elamur.ai/free/en/authors/sanjit-arunkumar-seshia/), [Rishabh Singh](https://md.research.elamur.ai/free/en/authors/rishabh-singh/), [Armando Solar-Lezama](https://md.research.elamur.ai/free/en/authors/armando-solar-lezama/), Emina Torlak and Abhishek Udupa · **Year:** 2013 · **Venue:** FMCAD 2013 · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1109/fmcad.2013.6679385) · [PDF](https://www.cis.upenn.edu/~alur/SyGuS13.pdf) · [OpenAlex](https://openalex.org/W2094878426)

**Citations:** 604 citations (OpenAlex, 2026-10-14) · [29](https://md.research.elamur.ai/free/en/papers/alur-2013-syntax-guided-synthesis/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Many recent synthesis tools, including program sketching, superoptimization, loop-free program synthesis and example-driven spreadsheet macros, let users restrict candidate programs syntactically as well as specifying them logically. These tools developed separately and had no common basis for comparison or shared back-ends. The authors define a single abstract problem, syntax-guided synthesis (SyGuS), built from logics and grammars rather than from any particular programming language.

A SyGuS instance has three parts: a background theory such as LIA, a correctness formula over a function f to be synthesized, and a context-free grammar describing the allowed expressions. A solution is any expression from the grammar that, when substituted for f, makes the formula valid in the theory.

The paper adapts the counter-example-guided inductive synthesis (CEGIS) loop in three ways: enumerative, symbolic (using Z3) and stochastic. It evaluates prototypes on Hacker's Delight, integer and array-search benchmarks. No single approach won everywhere. The aim is to give synthesis an SMT-LIB-style standard format and benchmark set.

## Key points
- A SyGuS instance consists of a background theory T, a specification ϕ whose free variables are universally quantified, and a grammar-defined candidate set L. The goal is to find e ∈ L such that ϕ[f/e] is valid modulo T.
- The authors note that asking whether such an expression exists in a context-free language cannot be reduced to checking the truth of a formula in T, even with extra quantifiers.
- The three CEGIS-based learners work differently:
  - **Enumerative:** builds expressions in order of size and prunes them using input-output examples.
  - **Symbolic:** encodes parse trees as SMT constraints and solves them with Z3.
  - **Stochastic:** samples expressions and then makes random single-edit moves across parse trees.
- Benchmark results:
  - Sketch failed on 11 of the hd benchmarks and handled array-search up to size 7; the enumerative solver handled array-search only up to size 4.
  - The enumerative solver solved the d5 variants of hd problems 11, 12, 14 and 15, which Sketch could not.
- Planned next steps are an input format called SYNTH-LIB (based on SMT-LIB2) with a public parser, a larger benchmark repository, and a SyGuS solver competition. The work was funded by NSF ExCAPE (CCF 1,138,996).

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of California, Berkeley](https://md.research.elamur.ai/free/en/universities/university-of-california-berkeley/) — University, Berkeley, United States · 243 works · 251,774 citations
- [University of Pennsylvania](https://md.research.elamur.ai/free/en/universities/university-of-pennsylvania/) — University, Philadelphia, United States · 241 works · 66,904 citations
- [Massachusetts Institute of Technology](https://md.research.elamur.ai/free/en/universities/massachusetts-institute-of-technology/) — University, Cambridge, United States · 274 works · 82,013 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works · [💻 Software](https://md.research.elamur.ai/free/en/shelves/computer-science/software/) · 150 works

🧭 Topics (1): [📐 Syntax & grammar formalisms](https://md.research.elamur.ai/free/en/topics/syntax-grammar/) · 225 works

## Cite

Cite as: Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak and Abhishek Udupa. 2013. Syntax-Guided Synthesis. FMCAD 2013.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{alur2013syntax,
  title = {{Syntax-Guided Synthesis}},
  author = {Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak and Abhishek Udupa},
  booktitle = {FMCAD 2013},
  year = {2013},
  doi = {10.1109/fmcad.2013.6679385},
  url = {https://doi.org/10.1109/fmcad.2013.6679385}
}
```

- [← previous NRC-Canada: Building the State-of-the-Art in Sentiment Analysis of Tweets](https://md.research.elamur.ai/free/en/papers/mohammad-2013-nrc-canada-building-state-art/)
- [next → Weakly Supervised Learning of Semantic Parsers for Mapping Instructions to Actions](https://md.research.elamur.ai/free/en/papers/artzi-2013-weakly-supervised-learning-semantic-parsers/)
- [↑ back to papers of 2013](https://md.research.elamur.ai/free/en/papers/2013/)

## References

27 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Satisfiability, 2009, vol. 4, ch. 8. [find](https://scholar.google.com/scholar?q=C%2E+Barrett%2C+R%2E+Sebastiani%2C+S%2E+A%2E+Seshia%2C+and+C%2E+Tinelli%2C+%E2%80%9CSatisfiability+modulo+theories%2C%E2%80%9D+in+Handbook+of+Satisfiability%2C+2009%2C+vol%2E+4%2C+ch%2E+8%2E)
2. L. M. de Moura and N. Bjørner, “Satisfiability modulo theories: Introduction and applications,” Commun. ACM, vol. 54, no. 9, 2011. [find](https://scholar.google.com/scholar?q=L%2E+M%2E+de+Moura+and+N%2E+Bj%C3%B8rner%2C+%E2%80%9CSatisfiability+modulo+theories%3A+Introduction+and+applications%2C%E2%80%9D+Commun%2E+ACM%2C+vol%2E+54%2C+no%2E+9%2C+2011%2E)
3. Z. Manna and R. Waldinger, “A deductive approach to program synthesis,” ACM TOPLAS, vol. 2, no. 1, pp. 90–121, 1980. [find](https://scholar.google.com/scholar?q=Z%2E+Manna+and+R%2E+Waldinger%2C+%E2%80%9CA+deductive+approach+to+program+synthesis%2C%E2%80%9D+ACM+TOPLAS%2C+vol%2E+2%2C+no%2E+1%2C+pp%2E+90%E2%80%93121%2C+1980%2E)
4. A. Solar-Lezama, R. Rabbah, R. Bodı́k, and K. Ebcioglu, “Programming by sketching for bit-streaming programs,” in PLDI, 2005. [find](https://scholar.google.com/scholar?q=A%2E+Solar%2DLezama%2C+R%2E+Rabbah%2C+R%2E+Bod%C4%B1%CC%81k%2C+and+K%2E+Ebcioglu%2C+%E2%80%9CProgramming+by+sketching+for+bit%2Dstreaming+programs%2C%E2%80%9D+in+PLDI%2C+2005%2E)
5. S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan, “Synthesis of loop-free programs,” SIGPLAN Not., vol. 46, pp. 62–73, June 2011. [find](https://scholar.google.com/scholar?q=S%2E+Gulwani%2C+S%2E+Jha%2C+A%2E+Tiwari%2C+and+R%2E+Venkatesan%2C+%E2%80%9CSynthesis+of+loop%2Dfree+programs%2C%E2%80%9D+SIGPLAN+Not%2E%2C+vol%2E+46%2C+pp%2E+62%E2%80%9373%2C+June+2011%2E)
6. S. Gulwani, W. R. Harris, and R. Singh, “Spreadsheet data manipulation using examples,” Commun. ACM, vol. 55, no. 8, pp. 97–105, 2012. [find](https://scholar.google.com/scholar?q=S%2E+Gulwani%2C+W%2E+R%2E+Harris%2C+and+R%2E+Singh%2C+%E2%80%9CSpreadsheet+data+manipulation+using+examples%2C%E2%80%9D+Commun%2E+ACM%2C+vol%2E+55%2C+no%2E+8%2C+pp%2E+97%E2%80%93105%2C+2012%2E)
7. S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, “Oracle-guided component-based program synthesis,” in ICSE, 2010, pp. 215–224. [find](https://scholar.google.com/scholar?q=S%2E+Jha%2C+S%2E+Gulwani%2C+S%2E+A%2E+Seshia%2C+and+A%2E+Tiwari%2C+%E2%80%9COracle%2Dguided+component%2Dbased+program+synthesis%2C%E2%80%9D+in+ICSE%2C+2010%2C+pp%2E+215%E2%80%93224%2E)
8. A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. Martin, and R. Alur, “T RANSIT : Specifying Protocols with Concolic Snippets,” in PLDI, 2013, pp. 287–296. [find](https://scholar.google.com/scholar?q=A%2E+Udupa%2C+A%2E+Raghavan%2C+J%2E+V%2E+Deshmukh%2C+S%2E+Mador%2DHaim%2C+M%2E+M%2E+Martin%2C+and+R%2E+Alur%2C+%E2%80%9CT+RANSIT+%3A+Specifying+Protocols+with+Concolic+Snippets%2C%E2%80%9D+in+PLDI%2C+2013%2C+pp%2E+287%E2%80%93296%2E)
9. S. Srivastava, S. Gulwani, and J. S. Foster, “From program verification to program synthesis,” in POPL, 2010, pp. 313–326. [find](https://scholar.google.com/scholar?q=S%2E+Srivastava%2C+S%2E+Gulwani%2C+and+J%2E+S%2E+Foster%2C+%E2%80%9CFrom+program+verification+to+program+synthesis%2C%E2%80%9D+in+POPL%2C+2010%2C+pp%2E+313%E2%80%93326%2E)
10. V. Kuncak, M. Mayer, R. Piskac, and P. Suter, “Software synthesis procedures,” Commun. ACM, vol. 55, no. 2, pp. 103–111, 2012. [find](https://scholar.google.com/scholar?q=V%2E+Kuncak%2C+M%2E+Mayer%2C+R%2E+Piskac%2C+and+P%2E+Suter%2C+%E2%80%9CSoftware+synthesis+procedures%2C%E2%80%9D+Commun%2E+ACM%2C+vol%2E+55%2C+no%2E+2%2C+pp%2E+103%E2%80%93111%2C+2012%2E)
11. E. Schkufza, R. Sharma, and A. Aiken, “[Stochastic superoptimization](https://md.research.elamur.ai/free/en/papers/schkufza-2012-stochastic-superoptimization/),” in ASPLOS, 2013, pp. 305–316.
12. M. Colón, S. Sankaranarayanan, and H. Sipma, “Linear invariant generation using non-linear constraint solving,” in CAV, 2003, pp. 420–432. [find](https://scholar.google.com/scholar?q=M%2E+Colo%CC%81n%2C+S%2E+Sankaranarayanan%2C+and+H%2E+Sipma%2C+%E2%80%9CLinear+invariant+generation+using+non%2Dlinear+constraint+solving%2C%E2%80%9D+in+CAV%2C+2003%2C+pp%2E+420%E2%80%93432%2E)
13. A. Rybalchenko, “Constraint solving for program verification: Theory and practice by example,” in CAV, 2010, pp. 57–71. [find](https://scholar.google.com/scholar?q=A%2E+Rybalchenko%2C+%E2%80%9CConstraint+solving+for+program+verification%3A+Theory+and+practice+by+example%2C%E2%80%9D+in+CAV%2C+2010%2C+pp%2E+57%E2%80%9371%2E)
14. R. Sharma, S. Gupta, B. Hariharan, A. Aiken, P. Liang, and A. V. Nori, “A data driven approach for algebraic loop invariants,” in ESOP, 2013, pp. 574–592. [find](https://scholar.google.com/scholar?q=R%2E+Sharma%2C+S%2E+Gupta%2C+B%2E+Hariharan%2C+A%2E+Aiken%2C+P%2E+Liang%2C+and+A%2E+V%2E+Nori%2C+%E2%80%9CA+data+driven+approach+for+algebraic+loop+invariants%2C%E2%80%9D+in+ESOP%2C+2013%2C+pp%2E+574%E2%80%93592%2E)
15. N. Bjørner, K. L. McMillan, and A. Rybalchenko, “On solving universally quantified Horn clauses,” in SAS, 2013, pp. 105–125. [find](https://scholar.google.com/scholar?q=N%2E+Bj%C3%B8rner%2C+K%2E+L%2E+McMillan%2C+and+A%2E+Rybalchenko%2C+%E2%80%9COn+solving+universally+quantified+Horn+clauses%2C%E2%80%9D+in+SAS%2C+2013%2C+pp%2E+105%E2%80%93125%2E)
16. A. Solar-Lezama, L. Tancau, R. Bodı́k, S. A. Seshia, and V. Saraswat, “Combinatorial sketching for finite programs,” in ASPLOS, 2006. [find](https://scholar.google.com/scholar?q=A%2E+Solar%2DLezama%2C+L%2E+Tancau%2C+R%2E+Bod%C4%B1%CC%81k%2C+S%2E+A%2E+Seshia%2C+and+V%2E+Saraswat%2C+%E2%80%9CCombinatorial+sketching+for+finite+programs%2C%E2%80%9D+in+ASPLOS%2C+2006%2E)
17. E. M. Gold, “Language identification in the limit,” Information and Control, vol. 10, no. 5, pp. 447–474, 1967. [find](https://scholar.google.com/scholar?q=E%2E+M%2E+Gold%2C+%E2%80%9CLanguage+identification+in+the+limit%2C%E2%80%9D+Information+and+Control%2C+vol%2E+10%2C+no%2E+5%2C+pp%2E+447%E2%80%93474%2C+1967%2E)
18. P. D. Summers, “A methodology for LISP program construction from examples,” J. ACM, vol. 24, no. 1, pp. 161–175, 1977. [find](https://scholar.google.com/scholar?q=P%2E+D%2E+Summers%2C+%E2%80%9CA+methodology+for+LISP+program+construction+from+examples%2C%E2%80%9D+J%2E+ACM%2C+vol%2E+24%2C+no%2E+1%2C+pp%2E+161%E2%80%93175%2C+1977%2E)
19. E. Y. Shapiro, Algorithmic Program Debugging. Cambridge, MA, USA: MIT Press, 1983. [find](https://scholar.google.com/scholar?q=E%2E+Y%2E+Shapiro%2C+Algorithmic+Program+Debugging%2E+Cambridge%2C+MA%2C+USA%3A+MIT+Press%2C+1983%2E)
20. D. Angluin and C. H. Smith, “Inductive inference: Theory and methods,” ACM Computing Surveys, vol. 15, pp. 237–269, Sep. 1983. [find](https://scholar.google.com/scholar?q=D%2E+Angluin+and+C%2E+H%2E+Smith%2C+%E2%80%9CInductive+inference%3A+Theory+and+methods%2C%E2%80%9D+ACM+Computing+Surveys%2C+vol%2E+15%2C+pp%2E+237%E2%80%93269%2C+Sep%2E+1983%2E)
21. T. M. Mitchell, Machine Learning. McGraw-Hill, 1997. [find](https://scholar.google.com/scholar?q=T%2E+M%2E+Mitchell%2C+Machine+Learning%2E+McGraw%2DHill%2C+1997%2E)
22. S. A. Seshia, “Sciduction: Combining induction, deduction, and structure for verification and synthesis,” in DAC, 2012, pp. 356–365. [find](https://scholar.google.com/scholar?q=S%2E+A%2E+Seshia%2C+%E2%80%9CSciduction%3A+Combining+induction%2C+deduction%2C+and+structure+for+verification+and+synthesis%2C%E2%80%9D+in+DAC%2C+2012%2C+pp%2E+356%E2%80%93365%2E)
23. D. Angluin, “Queries and concept learning,” Machine Learning, vol. 2, pp. 319–342, 1988. [find](https://scholar.google.com/scholar?q=D%2E+Angluin%2C+%E2%80%9CQueries+and+concept+learning%2C%E2%80%9D+Machine+Learning%2C+vol%2E+2%2C+pp%2E+319%E2%80%93342%2C+1988%2E)
24. A. Solar-Lezama, “[Program synthesis by sketching](https://md.research.elamur.ai/free/en/papers/lezama-2008-program-synthesis-sketching/),” Ph.D. dissertation, University of California, Berkeley, 2008.
25. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexample-guided abstraction refinement for symbolic model checking,” J. ACM, vol. 50, no. 5, pp. 752–794, 2003. [find](https://scholar.google.com/scholar?q=E%2E+M%2E+Clarke%2C+O%2E+Grumberg%2C+S%2E+Jha%2C+Y%2E+Lu%2C+and+H%2E+Veith%2C+%E2%80%9CCounterexample%2Dguided+abstraction+refinement+for+symbolic+model+checking%2C%E2%80%9D+J%2E+ACM%2C+vol%2E+50%2C+no%2E+5%2C+pp%2E+752%E2%80%93794%2C+2003%2E)
26. B. McKenzie, “Generating strings at random from a context free grammar,” 1997. [find](https://scholar.google.com/scholar?q=B%2E+McKenzie%2C+%E2%80%9CGenerating+strings+at+random+from+a+context+free+grammar%2C%E2%80%9D+1997%2E)
27. H. S. Warren, Hacker’s Delight. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2002. [find](https://scholar.google.com/scholar?q=H%2E+S%2E+Warren%2C+Hacker%E2%80%99s+Delight%2E+Boston%2C+MA%2C+USA%3A+Addison%2DWesley+Longman+Publishing+Co%2E%2C+Inc%2E%2C+2002%2E)

*Updated 3 November 2026*