@incollection(AlurBDF0JKMMRSSSSTU15,
 author       = {Rajeev Alur and Bod{\'{\i}}k, Rastislav and Eric Dallal and Dana Fisman and Pranav Garg and Garvit Juniwal and Kress{-}Gazit, Hadas and P. Madhusudan and Milo M. K. Martin and Mukund Raghothaman and Shambwaditya Saha and Sanjit A. Seshia and Rishabh Singh and Solar{-}Lezama, Armando and Emina Torlak and Abhishek Udupa},
 year         = {2015},
 title        = {Syntax-Guided Synthesis},
 booktitle    = {Dependable Software Systems Engineering},
 volume       = {40},
 publisher    = {{IOS} Press},
 pages        = {1--25},
 doi          = {10.3233/978-1-61499-495-4-1},
)
@inproceedings(AlurBJMRSSSTU13,
 author       = {Rajeev Alur and Bod{\'{\i}}k, Rastislav and Garvit Juniwal and Milo M. K. Martin and Mukund Raghothaman and Sanjit A. Seshia and Rishabh Singh and Solar{-}Lezama, Armando and Emina Torlak and Abhishek Udupa},
 year         = {2013},
 title        = {Syntax-guided synthesis},
 booktitle    = {Formal Methods in Computer-Aided Design, {FMCAD} 2013, Portland, OR, USA, October 20-23, 2013},
 pages        = {1--8},
)
@inproceedings(AlurCAV15,
 author       = {Rajeev Alur and Pavol Cern{\'{y}} and Arjun Radhakrishna},
 year         = {2015},
 title        = {Synthesis Through Unification},
 booktitle    = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}},
 pages        = {163--179},
 doi          = {10.1007/978-3-319-21668-3\_10},
)
@inproceedings(DBLP:conf/cav/AlurCR15,
 author       = {Rajeev Alur and Pavol Cern{\'{y}} and Arjun Radhakrishna},
 year         = {2015},
 title        = {Synthesis Through Unification},
 booktitle    = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}},
 pages        = {163--179},
 doi          = {10.1007/978-3-319-21668-3\_10},
)
@misc(smtlib,
 author       = {David R. Cok},
 year         = {2013},
 title        = {The SMT-LIBv2 Language and Tools: A Tutorial},
)
@inproceedings(GargLMN14,
 author       = {Pranav Garg and Christof L{\"{o}}ding and P. Madhusudan and Daniel Neider},
 year         = {2014},
 title        = {{ICE:} {A} Robust Framework for Learning Invariants},
 booktitle    = {Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings},
 pages        = {69--87},
 doi          = {10.1007/978-3-319-08867-9\_5},
)
@misc(GargNMR15,
 author       = {Pranav Garg and Daniel Neider and P. Madhusudan and  and Dan Roth},
 year         = {2015},
 title        = {Learning Invariants using Decision Trees and Implication Counterexamples},
 note         = {Technical report.},
)
@inproceedings(JeonQSF15,
 author       = {Jinseong Jeon and Xiaokang Qiu and Solar{-}Lezama, Armando and Jeffrey S. Foster},
 year         = {2015},
 title        = {Adaptive Concretization for Parallel Program Synthesis},
 booktitle    = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}},
 pages        = {377--394},
 doi          = {10.1007/978-3-319-21668-3\_22},
)
@inproceedings(Jha2010,
 author       = {Susmit Jha and Sumit Gulwani and Sanjit A. Seshia and Ashish Tiwari},
 year         = {2010},
 title        = {Oracle-guided Component-based Program Synthesis},
 booktitle    = {Proceedings of the 32Nd ACM/IEEE International Conference on Software Engineering - Volume 1},
 series       = {ICSE '10},
 pages        = {215--224},
 doi          = {10.1145/1806799.1806833},
)
@inproceedings(AleksICSE15,
 author       = {Aleksandar Milicevic and Joseph P. Near and Eunsuk Kang and Daniel Jackson},
 year         = {2015},
 title        = {Alloy*: {A} General-Purpose Higher-Order Relational Constraint Solver},
 booktitle    = {37th {IEEE/ACM} International Conference on Software Engineering, {ICSE} 2015, Florence, Italy, May 16-24, 2015, Volume 1},
 pages        = {609--619},
 doi          = {10.1109/ICSE.2015.77},
)
@misc(ICEDT,
 author       = {Daniel Neider and P. Madhusudan and Pranav Garg},
 year         = {2015},
 title        = {ICE DT: Learning Invariants using Decision Trees and Implication Counterexamples},
 note         = {Private Communication},
)
@misc(AlchemistCS,
 author       = {Daniel Neider and Shambwaditya Saha and P. Madhusudan},
 year         = {2015},
 title        = {Alchemist CS: An SMT-based synthesizer for Functions in Linear Integer Arithmetic},
 note         = {Private Communication},
)
@article(RaghothamanU14,
 author       = {Mukund Raghothaman and Abhishek Udupa},
 year         = {2014},
 title        = {Language to Specify Syntax-Guided Synthesis Problems},
 journal      = {CoRR},
 volume       = {abs/1405.5590},
)
@inproceedings(ReynoldsDKTB15,
 author       = {Andrew Reynolds and Morgan Deters and Viktor Kuncak and Cesare Tinelli and Clark W. Barrett},
 year         = {2015},
 title        = {Counterexample-Guided Quantifier Instantiation for Synthesis in {SMT}},
 booktitle    = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}},
 pages        = {198--216},
 doi          = {10.1007/978-3-319-21668-3\_12},
)
@misc(SosyToast,
 author       = {Heinz Riener and Rudiger Ehlers},
 year         = {2015},
 title        = {absTract sOlution Analyzing Synthesis Tool (System Description)},
 note         = {Private Communication},
)
@inproceedings(Saha0M15,
 author       = {Shambwaditya Saha and Pranav Garg and P. Madhusudan},
 year         = {2015},
 title        = {Alchemist: Learning Guarded Affine Functions},
 booktitle    = {Computer Aided Verification - 27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {I}},
 pages        = {440--446},
 doi          = {10.1007/978-3-319-21690-4\_26},
)
@misc(AlchemistCSDT,
 author       = {Shambwaditya Saha and Daniel Neider and P. Madhusudan},
 year         = {2015},
 title        = {Alchemist CS DT: Synthesizing Guarded Affine Functions using Constraint Solving and Decision-tree Learning},
 note         = {Private Communication},
)
@inproceedings(Solar-LezamaRBE05,
 author       = {Solar{-}Lezama, Armando and Rodric M. Rabbah and Bod{\'{\i}}k, Rastislav and Kemal Ebcioglu},
 year         = {2005},
 title        = {Programming by sketching for bit-streaming programs},
 booktitle    = {Proceedings of the {ACM} {SIGPLAN} 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005},
 pages        = {281--294},
 doi          = {10.1145/1065010.1065045},
)
@inproceedings(solar2006combinatorial,
 author       = {Solar-Lezama, Armando and Liviu Tancau and Rastislav Bodik and Vijay Saraswat and Sanjit Seshia},
 year         = {2006},
 title        = {Combinatorial Sketching for Finite Programs},
 booktitle    = {ASPLOS '06},
 publisher    = {ACM Press},
 address      = {San Jose, CA, USA},
 pages        = {404--415},
 doi          = {10.1145/1168857.1168907},
)
@article(SrivPts,
 author       = {Saurabh Srivastava and Sumit Gulwani and Jeffrey Foster},
 year         = {2010},
 title        = {From program verification to program synthesis},
 journal      = {POPL},
 doi          = {10.1145/1706299.1706337},
)
@inproceedings(starexec,
 author       = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli},
 year         = {2014},
 title        = {StarExec: {A} Cross-Community Infrastructure for Logic Solving},
 booktitle    = {Automated Reasoning - 7th International Joint Conference, {IJCAR} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 19-22, 2014. Proceedings},
 pages        = {367--373},
 doi          = {10.1007/978-3-319-08587-6\_28},
)
@inproceedings(TorlakB14,
 author       = {Emina Torlak and Bod\'{\i}k, Rastislav},
 year         = {2014},
 title        = {A lightweight symbolic virtual machine for solver-aided host languages},
 booktitle    = {PLDI},
 pages        = {54},
 doi          = {10.1145/2594291.2594340},
)