@misc(S,
 title        = "Specware",
 note         = "Http://www.specware.org",
)
@book(CLR01,
 author       = "T.~Cormen and C.~Leiserson and R.~Rivest and C.~Stein",
 year         = "2001",
 title        = "Introduction to Algorithms",
 edition      = "2nd",
 publisher    = "MIT Press",
)
@book(Dec03,
 author       = "R~Dechter",
 year         = "2003",
 title        = "Constraint Processing",
 publisher    = "Morgan Kauffman",
)
@inproceedings(GJTV11,
 author       = "S.~Gulwani and S.~Jha and A.~Tiwari and R.~Venkatesan",
 year         = "2011",
 title        = "Synthesis of loop-free programs",
 booktitle    = "PLDI",
 pages        = "62--73",
 doi          = "10.1145/2F1993498.1993506",
)
@article(Iba77,
 author       = "T.~Ibaraki",
 year         = "1977",
 title        = "The Power of Dominance Relations in Branch-and-Bound Algorithms",
 journal      = "J. ACM",
 volume       = "24",
 number       = "2",
 pages        = "264--279",
 doi          = "10.1145/2F322003.322010",
)
@inproceedings(IGMS10,
 author       = "S.~Itzhaky and S.~Gulwani and N.~Immerman and M.~Sagiv",
 year         = "2010",
 title        = "A simple inductive synthesis methodology and its applications",
 booktitle    = "OOPSLA",
 pages        = "36--46",
 doi          = "10.1145/2F1869459.1869463",
)
@incollection(Kre98,
 author       = "C.~Kreitz",
 year         = "1998",
 title        = "Program Synthesis",
 editor       = "W.~Bibel and P.~Schmitt",
 booktitle    = "Automated Deduction -- A Basis for Applications",
 chapter      = "III.2.5",
 volume       = "III",
 publisher    = "Kluwer",
 pages        = "105--134",
)
@inproceedings(Lei10,
 author       = "K.~R.~M. Leino",
 year         = "2010",
 title        = "Dafny: an automatic program verifier for functional correctness",
 booktitle    = "Proc. 16th intl. conf. on Logic for Prog., AI, \& Reasoning",
 series       = "LPAR",
 pages        = "348--370",
 doi          = "10.1007/2F978-3-642-17511-4\_20",
)
@phdthesis(Ned12,
 author       = "S.~Nedunuri",
 year         = "2012",
 title        = "Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms",
 school       = "Univ. of Texas at Austin",
)
@inproceedings(NC09,
 author       = "S.~Nedunuri and W.R. Cook",
 year         = "2009",
 title        = "Synthesis of Fast Programs for Maximum Segment Sum Problems",
 booktitle    = "Intl. Conf. on Generative Prog. and Component Engineering (GPCE)",
 doi          = "10.1145/2F1621607.1621626",
)
@article(NSC10b,
 author       = "S.~Nedunuri and D.~R. Smith and W.~R. Cook",
 year         = "2010",
 title        = "A Class of Greedy Algorithms and Its Relation to Greedoids",
 journal      = "Intl. Colloq. on Theoretical Aspects of Computing (ICTAC)",
 doi          = "10.1007/2F978-3-642-14808-8\_24",
)
@inproceedings(NSC12b,
 author       = "S.~Nedunuri and D.~R. Smith and W.~R. Cook",
 year         = "2012",
 title        = "Theory and Techniques for a Class of Efficient Breadth-First Search Algorithms",
 booktitle    = "Intl. Symp. on Formal Methods (FM)",
)
@inproceedings(PPS10,
 author       = "D.~Pavlovic and P.~Pepper and D.~R. Smith",
 year         = "2010",
 title        = "Formal Derivation of Concurrent Garbage Collectors.",
 booktitle    = "Math. of Program Constr. (MPC)",
 doi          = "10.1007/2F978-3-642-13321-3\_20",
)
@inproceedings(PBS11,
 author       = "Y.~Pu and R.~Bod\'{\i }k and S.~Srivastava",
 year         = "2011",
 title        = "Synthesis of first-order dynamic programming algorithms",
 booktitle    = "OOPSLA",
 pages        = "83--98",
 doi          = "10.1145/2F2048066.2048076",
)
@techreport(Smi88,
 author       = "D.~R. Smith",
 year         = "1988",
 title        = "Structure and Design of Global Search Algorithms",
 type         = "Tech. Rep.",
 number       = "Kes.U.87.12",
 institution  = "Kestrel Institute",
)
@article(Smi90,
 author       = "D.~R. Smith",
 year         = "1990",
 title        = "KIDS: A Semi-Automatic Program Development System",
 journal      = "IEEE Trans. on Soft. Eng., Spec. Issue on Formal Methods",
 volume       = "16",
 number       = "9",
 pages        = "1024--1043",
 doi          = "10.1109/2F32.58788",
)
@article(Smi10,
 author       = "D.~R. Smith",
 year         = "2010",
 title        = "Global Search Theory Revisited",
 journal      = "Unpublished",
)
@techreport(SPW95,
 author       = "D.~R. Smith and E.~A. Parra and S.~J. Westfold",
 year         = "1995",
 title        = "Synthesis of high-performance transportation schedulers",
 type         = "Technical Report",
 institution  = "Kestrel Institute",
)
@techreport(SW08,
 author       = "D.~R. Smith and S.~Westfold",
 year         = "2008",
 title        = "Synthesis of Propositional Satisfiability Solvers",
 type         = "Final Proj. Report",
 institution  = "Kestrel Institute",
)
@inproceedings(STBSS06,
 author       = "A.~Solar-Lezama and L.~Tancau and R.~Bodik and S.~Seshia and V.~Saraswat",
 year         = "2006",
 title        = "Combinatorial sketching for finite programs",
 booktitle    = "Proc. of the 12th intl. conf. on architectural support for prog. lang. and operating systems (ASPLOS)",
 pages        = "404--415",
 doi          = "10.1145/2F1168857.1168907",
)
@inproceedings(SGF10,
 author       = "S.~Srivastava and S.~Gulwani and J.~S. Foster",
 year         = "2010",
 title        = "From program verification to program synthesis",
 booktitle    = "POPL",
 pages        = "313--326",
 doi          = "10.1.1.148.395",
)
@inproceedings(VY08,
 author       = "M.~Vechev and E.~Yahav",
 year         = "2008",
 title        = "Deriving linearizable fine-grained concurrent objects",
 series       = "PLDI '08",
 pages        = "125--135",
 doi          = "10.1145/2F1375581.1375598",
)