citations.bib

@inproceedings{dpllt:04,
    author = {Ganzinger, Harald and Hagen, George and Nieuwenhuis, Robert and Oliveras, Albert and Tinelli, Cesare},
    booktitle = {CAV},
    pages = {175--188},
    series = {LNCS},
    title = {{DPLL(T): Fast Decision Procedures}},
    volume = {3114},
    year = {2004}
}

@InProceedings{smtlib2:10,
  author =	 {Clark Barrett and Aaron Stump and Cesare Tinelli},
  title =	 {{The SMT-LIB Standard: Version 2.0}},
  year =	 2010,
  booktitle =	 {Proceedings of the 8th International Workshop on
                  Satisfiability Modulo Theories (Edinburgh, England)},
  editor =	 {A.~Gupta and D.~Kroening},
}

@misc{racket/foreign,
  author = {Eli Barzilay},
  title = {{The Racket Foreign Interface}},
  howpublished = {\url{http://docs.racket-lang.org/foreign/}},
  year = {March 2012 (last accessed)}
}

@misc{racklog,
  author = {Dorai Sitaram},
  title = {{Racklog: Prolog-Style Logic Programming}},
  howpublished = {\url{http://docs.racket-lang.org/racklog/}},
  year = {May 2012 (last accessed)}
}

@misc{sbv,
  author = {Levent Erkok},
  title = {{SMT Based Verification: Symbolic Haskell theorem prover using SMT solving}},
  howpublished = {\url{http://hackage.haskell.org/package/sbv}},
  year = {June 2012 (last accessed)}
}

@misc{yices-painless,
  author = {Donald Stewart},
  title = {{yices-painless: An embedded language for programming the Yices SMT solver}},
  howpublished = {\url{http://hackage.haskell.org/package/yices-painless-0.1.2}},
  year = {March 2012 (last accessed)}
}

@techreport{racket,
  title       = {{Reference: Racket}},
  author      = {Matthew Flatt and PLT},
  number      = {PLT-TR-2010-1},
  institution = {PLT Inc.},
  year        = {2010},
  note        = {\url{http://racket-lang.org/tr1/}}
}

@incollection {z3,
   author = {de Moura, Leonardo and Bj{\o}rner, Nikolaj},
   affiliation = {Microsoft Research, One Microsoft Way Redmond WA 98074 USA},
   title = {{Z3: An Efficient SMT Solver}},
   booktitle = {TACAS}, 
   series = {LNCS},
   volume = {4963},
   year = {2008}
}

@TECHREPORT{yices,
    author = {Bruno Dutertre and Leonardo de Moura},
    title = {The {Yices SMT} solver},
    institution = {},
    year = {2006}
}

@inproceedings{cvc3,
  author    = "Clark Barrett and Cesare Tinelli",
  title     = "{CVC3}",
  booktitle = "CAV",
  series    = "LNCS",
  volume    = 4590,
  editor    = "Werner Damm and Holger Hermanns",
  pages     = "298--302",
  year      = 2007,
}

@inproceedings{Gulwani:08,
 author = {Gulwani, Sumit and Srivastava, Saurabh and Venkatesan, Ramarathnam},
 title = {Program analysis as constraint solving},
 booktitle = {PLDI},
 year = {2008},
 pages = {281--292},
 numpages = {12},
} 

@inproceedings{Godefroid:08,
    author = {Patrice Godefroid and Michael Y. Levin and David A
              Molnar},
    title = {{Automated Whitebox Fuzz Testing}},
    booktitle = {{NDSS}},
    year = {2008},
    URL = {http://www.truststc.org/pubs/499.html}
}

@article{Armando:09,
 author = {Armando, Alessandro and Mantovani, Jacopo and Platania, Lorenzo},
 title = {{Bounded model checking of software using SMT solvers instead of SAT solvers}},
 journal = {STTT},
 volume = {11},
 number = {1},
 year = {2009},
 issn = {1433-2779},
 pages = {69--83},
 numpages = {15},
} 

@inproceedings{Tobin-Hochstadt:11,
 author = {Tobin-Hochstadt, Sam and St-Amour, Vincent and Culpepper, Ryan and Flatt, Matthew and Felleisen, Matthias},
 title = {Languages as libraries},
 booktitle = {PLDI},
 year = {2011},
 pages = {132--141},
 numpages = {10},
}

@inproceedings{scalaz3,
  author    = {Ali Sinan K{\"o}ksal and
               Viktor Kuncak and
               Philippe Suter},
  title     = {{Scala to the Power of Z3: Integrating SMT and Programming}},
  booktitle = {ICAD},
  location  = {Wroclaw, Poland},
  year      = {2011},
  pages     = {400-406},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22438-6_30},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{mbqi,
 author = {Ge, Yeting and de Moura, Leonardo},
 title = {{Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories}},
 booktitle = {CAV},
 year = {2009},
 location = {Grenoble, France},
 pages = {306--320},
 numpages = {15},
} 

@article{halpern91,
    author = {Joseph Y. Halpern},
    title = {{Presburger Arithmetic With Unary Predicates is $\Pi^1_1$ Complete}},
    journal = {Journal of Symbolic Logic},
    year = {1991},
    volume = {56},
    pages = {56--2}
}

@inproceedings{sat-recursive,
 author = {Suter, Philippe and K\"{o}ksal, Ali Sinan and Kuncak, Viktor},
 title = {{Satisfiability Modulo Recursive Programs}},
 booktitle = {SAS},
 year = {2011},
 pages = {298--315},
 numpages = {18},
} 

@misc{z3py,
  author = {{Microsoft Research}},
  title = {{Z3Py - Python interface for the Z3 Theorem Prover}},
  howpublished = {\url{http://rise4fun.com/z3py/}},
  year = {May 2012 (last accessed)}
}

@book{sicp,
  author = {Harold Abelson and Gerald Jay Sussman and Julie Sussman},
  title = {{Structure and Interpretation of Computer Programs}},
  publisher = {MIT Press},
  year = {1996},
  edition = {2nd}
}

@misc{gecode,
  author = {{Gecode Team}},
  title = {{Gecode: Generic Constraint Development Environment}},
  howpublished = {\url{http://www.gecode.org}},
  year = {May 2012 (last accessed)},
}

@misc{JaCoP,
  author = {{JaCoP Team}},
  title = {{JaCoP - Java Constraint Programming solver}},
  howpublished = {\url{http://jacop.osolpro.com/}},
  year = {May 2012 (last accessed)},
}

@inproceedings{e-matching,
 author = {de Moura, Leonardo and Bj{\o}rner, Nikolaj},
 title = {{Efficient E-Matching for SMT Solvers}},
 booktitle = {CADE-21},
 year = {2007},
 pages = {183--198},
} 

@article{mastermind,
 author = {Knuth, Donald E.},
 title = {{The Computer as a Master Mind}},
 journal = {Journal of Recreational Mathematics},
 volume = {9},
 number = {1},
 year = {1976--77},
 pages = {1--6},
} 

@article{mastermindnpc,
    author = {Jeff Stuckman and Guo-qiang Zhang},
    title = {{Mastermind is NP-Complete}},
    journal = {INFOCOMP Journal of Computer Science},
    year = {2006},
    volume = {5},
    pages = {25--28}
}

@misc{numbermind,
  author = {{Colin Hughes}},
  title = {{Problem 185 - Project Euler}},
  howpublished = {\url{http://projecteuler.net/problem=185}},
  year = {May 2012 (last accessed)}
}

@article{scheme-r5rs,
    editor = {Kelsey, Richard and Clinger, William and Rees, Jonathan},
    journal = {ACM SIGPLAN Notices},
    number = {9},
    pages = {26--76},
    title = {{Fifth Revised Report on the Algorithmic Language Scheme}},
    volume = {33},
    year = {1998}
}

@article{scheme-r6rs,
    author = {Michael Sperber and R. Kent Dybvig and Matthew Flatt and Anton van Straaten and Robby Findler and Jocob Matthews},
    title = {{Revised$^6$ Report on the Algorithmic Language Scheme}},
    journal = {Journal of Functional Programming},
    volume = {19},
    number = {S1},
    year = {2009},
    pages = {1-301},
}

@inproceedings{sat-npcomplete,
 author = {Cook, Stephen A.},
 title = {The complexity of theorem-proving procedures},
 booktitle = {STOC},
 year = {1971},
 pages = {151--158},
 numpages = {8},
}

@incollection{karp21,
  author = {Karp, Richard M.},
  booktitle = {Complexity of Computer Computations},
  editor = {Miller, R. and Thatcher, J.},
  pages = {85--103},
  title = {Reducibility among combinatorial problems},
  year = {1972}
}

@article{dpll1,
 author = {Davis, Martin and Putnam, Hilary},
 title = {{A Computing Procedure for Quantification Theory}},
 journal = {Journal of the ACM},
 volume = {7},
 number = {3},
 year = {1960},
 pages = {201--215},
}

@article{dpll2,
 author = {Davis, Martin and Logemann, George and Loveland, Donald},
 title = {{A Machine Program for Theorem-Proving}},
 journal = {Communications of the ACM},
 volume = {5},
 number = {7},
 year = {1962},
 pages = {394--397},
 numpages = {4},
}

@inproceedings{walksat,
    author = {Bart Selman and Henry A. Kautz and Bram Cohen},
    title = {{Local Search Strategies for Satisfiability Testing}},
    booktitle = {DIMACS Series in Discrete Mathematics and Theoretical Computer Science},
    year = {1996},
    pages = {521--532}
}

@inproceedings{chaff,
    author = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik},
    title = {{Chaff: Engineering an Efficient SAT Solver}},
    booktitle = {DAC},
    year = {2001},
    pages = {530--535}
}

@inproceedings{grasp,
    author = {Jo{\~a}o P. Marques Silva and Karem A. Sakallah},
    title = {{GRASP - A New Search Algorithm for Satisfiability}},
    booktitle = {ICAD},
    year = {1996},
    pages = {220--227}
}

@inproceedings{minisat,
    author = {Niklas E\'{e}n and Niklas Sörensson},
    title = {{An Extensible SAT-solver}},
    booktitle = {SAT},
    year = {2003},
    pages = {502--508}
}

@inproceedings{satplan,
 author = {Kautz, Henry and Selman, Bart},
 title = {Planning as satisfiability},
 booktitle = {ECAI},
 year = {1992},
 pages = {359--363},
} 

@misc{zypper,
  author = {{OpenSUSE Team}},
  title = {{Portal:Libzypp - OpenSUSE}},
  howpublished = {\url{http://en.opensuse.org/Portal:Libzypp}},
  year = {June 2012 (last accessed)}
}

@inproceedings{slam,
 author = {Ball, Thomas and Majumdar, Rupak and Millstein, Todd and Rajamani, Sriram K.},
 title = {{Automatic predicate abstraction of C programs}},
 booktitle = {PLDI},
 year = {2001},
 pages = {203--213},
} 

@article{proc-verification,
    author = {Randal E. Bryant and Steven German and Miroslav N. Velev},
    title = {Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic},
    journal = {ACM Transactions on Computational Logic},
    year = {1999},
    volume = {2},
    pages = {37--53}
}

@inproceedings{uclid,
    author = {Shuvendu K. Lahiri and Sanjit A. Seshia},
    title = {{The UCLID Decision Procedure}},
    booktitle = {CAV},
    year = {2004},
    pages = {475--478},
}

@article{abstract-dpll,
 author = {Nieuwenhuis, Robert and Oliveras, Albert and Tinelli, Cesare},
 title = {{Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)}},
 journal = {Journal of the ACM},
 volume = {53},
 number = {6},
 year = {2006},
 pages = {937--977},
}