@inproceedings(AlurETAL13SyntaxguidedSynthesis,
 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    = {FMCAD},
 publisher    = {{IEEE}},
 pages        = {1--17},
)
@inproceedings(alur2016results,
 author       = {Rajeev Alur and Dana Fisman and Rishabh Singh and Solar{-}Lezama, Armando},
 year         = {2015},
 title        = {Results and Analysis of SyGuS-Comp'15},
 booktitle    = {Proceedings Fourth Workshop on Synthesis, {SYNT} 2015, San Francisco, CA, USA, 18th July 2015.},
 pages        = {3--26},
 doi          = {10.4204/EPTCS.202.3},
)
@inproceedings(DBLP:journals/corr/AlurFSS16a,
 author       = {Rajeev Alur and Dana Fisman and Rishabh Singh and Solar{-}Lezama, Armando},
 year         = {2016},
 title        = {SyGuS-Comp 2016: Results and Analysis},
 booktitle    = {Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016.},
 pages        = {178--202},
 doi          = {10.4204/EPTCS.229.13},
)
@inproceedings(alurscaling,
 author       = {Rajeev Alur and Arjun Radhakrishna and Abhishek Udupa},
 year         = {2017},
 title        = {Scaling Enumerative Program Synthesis via Divide and Conquer},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
 pages        = {319--336},
 doi          = {10.1007/978-3-319-21690-4_26},
)
@inproceedings(BanEtAl-IJCAR-16,
 author       = {Kshitij Bansal and Andrew Reynolds and Clark W. Barrett and Cesare Tinelli},
 year         = {2016},
 title        = {A New Decision Procedure for Finite Sets and Cardinality Constraints in {SMT}},
 booktitle    = {Automated Reasoning - 8th International Joint Conference, {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
 pages        = {82--98},
 doi          = {10.1007/978-3-319-40229-1_7},
)
@inproceedings(CVC4-CAV-11,
 author       = {Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 booktitle    = {Computer Aided Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1_14},
)
@article(DBLP:journals/entcs/BarrettST07,
 author       = {Clark Barrett and Igor Shikanian and Cesare Tinelli},
 year         = {2007},
 title        = {An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {174},
 number       = {8},
 pages        = {23--37},
 doi          = {10.1016/j.entcs.2006.11.037},
)
@inproceedings(Bjoerner10LinearQuantifierEliminationAsAbstractDecision,
 author       = {Bj{\o}rner, Nikolaj},
 year         = {2010},
 title        = {Linear Quantifier Elimination as an Abstract Decision Procedure},
 editor       = {J{\"{u}}rgen Giesl and Reiner H{\"{a}}hnle},
 booktitle    = {IJCAR},
 series       = {LNCS},
 volume       = {6173},
 publisher    = {Springer},
 pages        = {316--330},
 doi          = {10.1007/978-3-642-14203-1_27},
)
@inproceedings(DBLP:conf/lpar/BjornerJ15,
 author       = {Bj{\o}rner, Nikolaj and Mikol{\'{a}}s Janota},
 year         = {2015},
 title        = {Playing with Quantified Satisfaction},
 booktitle    = {20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, {LPAR} 2015, Suva, Fiji, November 24-28, 2015.},
 pages        = {15--27},
 url          = {http://www.easychair.org/publications/paper/252316},
)
@article(brain2014deciding,
 author       = {Martin Brain and Vijay D’Silva and Alberto Griggio and Leopold Haller and Daniel Kroening},
 year         = {2014},
 title        = {Deciding Floating-point Logic with Abstract Conflict Driven Clause Learning},
 journal      = {Formal Methods in System Design},
 volume       = {45},
 number       = {2},
 pages        = {213--245},
 doi          = {10.1007/s10703-013-0203-7},
)
@inproceedings(cooper1972,
 author       = {D. C. Cooper},
 year         = {1972},
 title        = {Theorem Proving in Arithmetic without Multiplication},
 booktitle    = {Machine Intelligence, pages 91–100},
)
@inproceedings(dutertresolving,
 author       = {Bruno Dutertre},
 year         = {2015},
 title        = {Solving Exists/Forall Problems With Yices},
 booktitle    = {Workshop on Satisfiability Modulo Theories},
)
@inproceedings(DBLP:conf/ijcai/FarzanK16,
 author       = {Azadeh Farzan and Zachary Kincaid},
 year         = {2016},
 title        = {Linear Arithmetic Satisfiability via Strategy Improvement},
 booktitle    = {Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, {IJCAI} 2016, New York, NY, USA, 9-15 July 2016},
 pages        = {735--743},
 url          = {http://www.ijcai.org/Abstract/16/110},
)
@inproceedings(DBLP:conf/lpar/FedyukovichGS15,
 author       = {Grigory Fedyukovich and Arie Gurfinkel and Natasha Sharygina},
 year         = {2015},
 title        = {Automated Discovery of Simulation Between Programs},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28, 2015, Proceedings},
 pages        = {606--621},
 doi          = {10.1007/978-3-662-48899-7_42},
)
@book(FerranteRackoff79ComputationalComplexityLogicalTheories,
 author       = {Jeanne Ferrante and Charles W. Rackoff},
 year         = {1979},
 title        = {The Computational Complexity of Logical Theories},
 series       = {Lecture Notes in Mathematics},
 volume       = {718},
 publisher    = {Springer},
 doi          = {10.1007/BFb0062845},
)
@inproceedings(ganzinger2003new,
 author       = {Harald Ganzinger and Konstantin Korovin},
 year         = {2003},
 title        = {New directions in instantiation-based theorem proving},
 booktitle    = {Logic in Computer Science, 2003.},
 organization = {IEEE},
 doi          = {10.1109/LICS.2003.1210045},
)
@inproceedings(DBLP:conf/popl/Gulwani11,
 author       = {Sumit Gulwani},
 year         = {2011},
 title        = {Automating string processing in spreadsheets using input-output examples},
 booktitle    = {Proceedings of the 38th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2011, Austin, TX, USA, January 26-28, 2011},
 pages        = {317--330},
 doi          = {10.1145/1926385.1926423},
)
@inproceedings(gulwani2011synthesis,
 author       = {Sumit Gulwani and Susmit Jha and Ashish Tiwari and Ramarathnam Venkatesan},
 year         = {2011},
 title        = {Synthesis of loop-free programs},
 booktitle    = {Proceedings of the 32nd {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2011, San Jose, CA, USA, June 4-8, 2011},
 pages        = {62--73},
 doi          = {10.1145/1993498.1993506},
)
@incollection(komuravelli2014smt,
 author       = {Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki},
 year         = {2014},
 title        = {{SMT}-based Model Checking for Recursive Programs},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 doi          = {10.1007/978-3-319-08867-9_2},
)
@inproceedings(DBLP:conf/pldi/KuncakMPS10,
 author       = {Viktor Kuncak and Mika{\"{e}}l Mayer and Ruzica Piskac and Philippe Suter},
 year         = {2010},
 title        = {Complete functional synthesis},
 booktitle    = {Proceedings of the 2010 {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2010, Toronto, Ontario, Canada, June 5-10, 2010},
 pages        = {316--329},
 doi          = {10.1145/1806596.1806632},
)
@inproceedings(LiangRTBD14,
 author       = {Tianyi Liang and Andrew Reynolds and Cesare Tinelli and Clark Barrett and Morgan Deters},
 year         = {2014},
 title        = {A {DPLL(T)} Theory Solver for a Theory of Strings and Regular Expressions},
 booktitle    = {Computer Aided Verification - 26th International Conference, {CAV} 2014},
 pages        = {646--662},
 doi          = {10.1007/978-3-319-08867-9_43},
)
@article(Loos93applyinglinear,
 author       = {R{\"{u}}diger Loos and Volker Weispfenning},
 year         = {1993},
 title        = {Applying Linear Quantifier Elimination},
 journal      = {Comput. J.},
 volume       = {36},
 number       = {5},
 pages        = {450--462},
 doi          = {10.1093/comjnl/36.5.450},
)
@inproceedings(Monniaux10QuantifierEliminationLazyModelEnumeration,
 author       = {David Monniaux},
 year         = {2010},
 title        = {Quantifier Elimination by Lazy Model Enumeration},
 booktitle    = {Computer Aided Verification, 22nd International Conference, {CAV} 2010, Edinburgh, UK, July 15-19, 2010. Proceedings},
 pages        = {585--599},
 doi          = {10.1007/978-3-642-14295-6_51},
)
@inproceedings(MouraBjoerner07EfficientEmatchingSmtSolvers,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2007},
 title        = {Efficient E-Matching for {SMT} Solvers},
 editor       = {Frank Pfenning},
 booktitle    = {CADE},
 series       = {LNCS},
 volume       = {4603},
 publisher    = {Springer},
 pages        = {183--198},
 doi          = {10.1007/978-3-540-73595-3_13},
)
@article(nieuwenhuis2006solving,
 author       = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
 year         = {2006},
 title        = {Solving {SAT} and {SAT} Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(\emph{T})},
 journal      = {J. {ACM}},
 volume       = {53},
 number       = {6},
 pages        = {937--977},
 doi          = {10.1145/1217856.1217859},
)
@inproceedings(DBLP:conf/tacas/PreinerNB17,
 author       = {Mathias Preiner and Aina Niemetz and Armin Biere},
 year         = {2017},
 title        = {Counterexample-Guided Model Synthesis},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
 pages        = {264--280},
 doi          = {10.1007/978-3-662-48899-7_42},
)
@inproceedings(DBLP:conf/sat/RabeS16,
 author       = {Markus N. Rabe and Sanjit A. Seshia},
 year         = {2016},
 title        = {Incremental Determinization},
 booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
 pages        = {375--392},
 doi          = {10.1007/978-3-319-40970-2_23},
)
@inproceedings(reynolds2015decision,
 author       = {Andrew Reynolds and Jasmin Christian Blanchette},
 year         = {2016},
 title        = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
 booktitle    = {Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, {IJCAI} 2016, New York, NY, USA, 9-15 July 2016},
 pages        = {4205--4209},
 url          = {http://www.ijcai.org/Abstract/16/631},
)
@inproceedings(ReynoldsDKBT15Cav,
 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},
)
@article(InstLA2016,
 author       = {Andrew Reynolds and Tim King and Viktor Kuncak},
 year         = {2017},
 title        = {Solving quantified linear arithmetic by counterexample-guided instantiation},
 journal      = {Formal Methods in System Design},
 doi          = {10.1007/s10703-017-0290-y},
)
@article(ReynoldsFMSD2017,
 author       = {Andrew Reynolds and Viktor Kuncak and Cesare Tinelli and Clark Barrett and Morgan Deters},
 year         = {2017},
 title        = {Refutation-based synthesis in SMT},
 journal      = {Formal Methods in System Design},
 doi          = {10.1007/978-3-540-30142-4_22},
)
@inproceedings(DBLP:conf/cav/ReynoldsWBBLT17,
 author       = {Andrew Reynolds and Maverick Woo and Clark Barrett and David Brumley and Tianyi Liang and Cesare Tinelli},
 year         = {2017},
 title        = {Scaling Up {DPLL(T)} String Solvers Using Context-Dependent Simplification},
 booktitle    = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
 pages        = {453--474},
 doi          = {10.1007/978-3-319-63390-9_24},
)
@article(SolarLezama13ProgramSketching,
 author       = {Solar{-}Lezama, Armando},
 year         = {2013},
 title        = {Program sketching},
 journal      = {{STTT}},
 volume       = {15},
 number       = {5-6},
 pages        = {475--495},
 doi          = {10.1007/s10009-012-0249-7},
)
@inproceedings(sturm2011verification,
 author       = {Thomas Sturm and Ashish Tiwari},
 year         = {2011},
 title        = {Verification and synthesis using real quantifier elimination},
 booktitle    = {Symbolic and Algebraic Computation, International Symposium, {ISSAC} 2011 (co-located with {FCRC} 2011), San Jose, CA, USA, June 7-11, 2011, Proceedings},
 pages        = {329--336},
 doi          = {10.1145/1993886.1993935},
)
@inproceedings(tiwari2015program,
 author       = {Ashish Tiwari and Adri{\`{a}} Gasc{\'{o}}n and Bruno Dutertre},
 year         = {2015},
 title        = {Program Synthesis Using Dual Interpretation},
 booktitle    = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
 pages        = {482--497},
 doi          = {10.1007/978-3-319-21401-6_33},
)
@inproceedings(udupa2013transit,
 author       = {Abhishek Udupa and Arun Raghavan and Jyotirmoy V. Deshmukh and Mador{-}Haim, Sela and Milo M. K. Martin and Rajeev Alur},
 year         = {2013},
 title        = {{TRANSIT:} specifying protocols with concolic snippets},
 booktitle    = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} '13, Seattle, WA, USA, June 16-19, 2013},
 pages        = {287--296},
 doi          = {10.1145/2462156.2462174},
)
@inproceedings(DBLP:conf/aips/WangDCK16,
 author       = {Yue Wang and Neil T. Dantam and Swarat Chaudhuri and Lydia E. Kavraki},
 year         = {2016},
 title        = {Task and Motion Policy Synthesis as Liveness Games},
 booktitle    = {Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling, {ICAPS} 2016, London, UK, June 12-17, 2016.},
 pages        = {536},
)
@article(wintersteiger2013efficiently,
 author       = {Christoph M Wintersteiger and Youssef Hamadi and De Moura, Leonardo},
 year         = {2013},
 title        = {Efficiently Solving Quantified Bit-vector Formulas},
 journal      = {Formal Methods in System Design},
 volume       = {42},
 number       = {1},
 pages        = {3--23},
 doi          = {10.1007/s10703-012-0156-2},
)