Elamur Research⌕
☰
home / papers / 2013 / Syntax-Guided Synthesis

Syntax-Guided Synthesis

Paper · 2013 · Rajeev Alur, Rastislav Bodik, Garvit Juniwal et al.

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, BerkeleyBerkeley · United States243 works · 251,774 citations🎓University of PennsylvaniaPhiladelphia · United States241 works · 66,904 citations🎓Massachusetts Institute of TechnologyCambridge · United States274 works · 82,013 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 worksSoftware · 150 works

🧭 Topics 1Research subjects and languages the work is about.Syntax & grammar formalisms · 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.

@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}
}

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
  2. L. M. de Moura and N. Bjørner, “Satisfiability modulo theories: Introduction and applications,” Commun. ACM, vol. 54, no. 9, 2011. find
  3. Z. Manna and R. Waldinger, “A deductive approach to program synthesis,” ACM TOPLAS, vol. 2, no. 1, pp. 90–121, 1980. find
  4. A. Solar-Lezama, R. Rabbah, R. Bodı́k, and K. Ebcioglu, “Programming by sketching for bit-streaming programs,” in PLDI, 2005. find
  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
  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
  7. S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, “Oracle-guided component-based program synthesis,” in ICSE, 2010, pp. 215–224. find
  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
  9. S. Srivastava, S. Gulwani, and J. S. Foster, “From program verification to program synthesis,” in POPL, 2010, pp. 313–326. find
  10. V. Kuncak, M. Mayer, R. Piskac, and P. Suter, “Software synthesis procedures,” Commun. ACM, vol. 55, no. 2, pp. 103–111, 2012. find
  11. E. Schkufza, R. Sharma, and A. Aiken, “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
  13. A. Rybalchenko, “Constraint solving for program verification: Theory and practice by example,” in CAV, 2010, pp. 57–71. find
  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
  15. N. Bjørner, K. L. McMillan, and A. Rybalchenko, “On solving universally quantified Horn clauses,” in SAS, 2013, pp. 105–125. find
  16. A. Solar-Lezama, L. Tancau, R. Bodı́k, S. A. Seshia, and V. Saraswat, “Combinatorial sketching for finite programs,” in ASPLOS, 2006. find
  17. E. M. Gold, “Language identification in the limit,” Information and Control, vol. 10, no. 5, pp. 447–474, 1967. find
  18. P. D. Summers, “A methodology for LISP program construction from examples,” J. ACM, vol. 24, no. 1, pp. 161–175, 1977. find
  19. E. Y. Shapiro, Algorithmic Program Debugging. Cambridge, MA, USA: MIT Press, 1983. find
  20. D. Angluin and C. H. Smith, “Inductive inference: Theory and methods,” ACM Computing Surveys, vol. 15, pp. 237–269, Sep. 1983. find
  21. T. M. Mitchell, Machine Learning. McGraw-Hill, 1997. find
  22. S. A. Seshia, “Sciduction: Combining induction, deduction, and structure for verification and synthesis,” in DAC, 2012, pp. 356–365. find
  23. D. Angluin, “Queries and concept learning,” Machine Learning, vol. 2, pp. 319–342, 1988. find
  24. A. Solar-Lezama, “Program synthesis by 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
  26. B. McKenzie, “Generating strings at random from a context free grammar,” 1997. find
  27. H. S. Warren, Hacker’s Delight. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2002. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/alur-2013-syntax-guided-synthesis/