@inproceedings(11-armand-smt-coq,
 author       = "Micha{\"e}l Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Thery and Benjamin Werner",
 year         = "2011",
 title        = "A Modular Integration of {SAT/SMT} Solvers to {Coq} through Proof Witnesses",
 booktitle    = "CPP '11",
 series       = "LNCS",
 volume       = "7086",
 publisher    = "Springer",
 pages        = "135--150",
 doi          = "10.1007/978-3-642-25379-9\_12",
)
@inproceedings(09-audemard-glucose,
 author       = "Gilles Audemard and Laurent Simon",
 year         = "2009",
 title        = "Predicting Learnt Clauses Quality in Modern {SAT} Solvers",
 booktitle    = "IJCAI '09",
 publisher    = "IJCAI Organization",
 pages        = "399--404",
)
@inproceedings(12-biere-lingeling,
 author       = "Armin Biere",
 year         = "2012",
 title        = "Lingeling and Friends Entering the {SAT} Challenge 2012",
 booktitle    = "Proc. {SAT} Challenge 2012",
 series       = "Department of Computer Science Series of Publications B",
 volume       = "B-2012-2",
 publisher    = "University of Helsinki",
 pages        = "33--34",
)
@inproceedings(11-bohme-smt,
 author       = "Sascha B{\"{o}}hme and Anthony Fox and Thomas Sewell and Tjark Weber",
 year         = "2011",
 title        = "Reconstruction of {Z3}'s Bit-Vector Proofs in {HOL4} and {Isabelle/HOL}",
 booktitle    = "CPP '11",
 series       = "LNCS",
 volume       = "7086",
 publisher    = "Springer",
 pages        = "183--198",
 doi          = "10.1007/978-3-642-25379-9\_15",
)
@inproceedings(06-boyer-acl2h,
 author       = "Robert S. Boyer and Warren A. {Hunt, Jr.}",
 year         = "2006",
 title        = "Function Memoization and Unique Object Representation for {ACL2} Functions",
 booktitle    = "ACL2 '06",
 publisher    = "ACM",
 pages        = "81--89",
 doi          = "10.1145/1217975.1217992",
)
@inproceedings(02-boyer-stobjs,
 author       = "Robert S. Boyer and J Strother Moore",
 year         = "2002",
 title        = "Single-Threaded Objects in {ACL2}",
 booktitle    = "PADL '02",
 series       = "LNCS",
 volume       = "2257",
 publisher    = "Springer",
 pages        = "9--27",
 doi          = "10.1007/3-540-45587-6\_3",
)
@inproceedings(12-bradley-ic3,
 author       = "Aaron R. Bradley",
 year         = "2012",
 title        = "Understanding {IC3}",
 booktitle    = "SAT '12",
 series       = "LNCS",
 volume       = "7317",
 publisher    = "Springer",
 pages        = "1--14",
 doi          = "10.1007/978-3-642-31612-8\_1",
)
@inproceedings(10-brayton-abc,
 author       = "Robert Brayton and Alan Mishchenko",
 year         = "2010",
 title        = "{ABC}: An Academic Industrial-Strength Verification Tool",
 booktitle    = "CAV '10",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 pages        = "24--40",
 doi          = "10.1007/978-3-642-14295-6\_5",
)
@inproceedings(06-brummayer-without-blowup,
 author       = "Robert Brummayer and Armin Biere",
 year         = "2006",
 title        = "Local Two-Level And-Inverter Graph Minimization without Blowup",
 booktitle    = "MEMICS '06",
)
@inproceedings(09-brummayer-fuzzing,
 author       = "Robert Brummayer and Armin Biere",
 year         = "2009",
 title        = "Fuzzing and Delta-Debugging {SMT} Solvers",
 booktitle    = "SMT '09",
 publisher    = "ACM",
 pages        = "1--5",
 doi          = "10.1145/1670412.1670413",
)
@inproceedings(07-chatterjee-resolution,
 author       = "Satrajit Chatterjee and Alan Mishchenko and Robert Brayton and Andreas Kuehlmann",
 year         = "2007",
 title        = "On resolution proofs for combinational equivalence",
 booktitle    = "DAC '07",
 publisher    = "ACM",
 pages        = "600--605",
 doi          = "10.1145/1278480.1278631",
)
@inproceedings(10-darbari-sat,
 author       = "Ashish Darbari and Bernd Fischer and Jo$\mathaccentV {tilde}07E{\textrm {a}}$o Marques-Silva",
 year         = "2010",
 title        = "Industrial-Strength Certified {SAT} Solving through Verified {SAT} Proof Checking",
 booktitle    = "ICTAC '10",
 series       = "LNCS",
 volume       = "6255",
 publisher    = "Springer",
 pages        = "260--274",
 doi          = "10.1007/978-3-642-14808-8\_18",
)
@inproceedings(04-davis-osets,
 author       = "Jared Davis",
 year         = "2004",
 title        = "Finite Set Theory based on Fully Ordered Lists",
 booktitle    = "ACL2 '04",
)
@inproceedings(11-een-pdr,
 author       = "Niklas E{\'e}n and Alan Mishchenko and Robert K. Brayton",
 year         = "2011",
 title        = "Efficient implementation of property directed reachability",
 booktitle    = "FMCAD '11",
 publisher    = "FMCAD, Inc.",
 pages        = "125--134",
)
@inproceedings(07-een-synthesis,
 author       = "Niklas E{\'e}n and Alan Mishchenko and Niklas S{\"o}rensson",
 year         = "2007",
 title        = "Applying Logic Synthesis for Speeding Up {SAT}",
 booktitle    = "SAT '07",
 series       = "LNCS",
 volume       = "4501",
 publisher    = "Springer",
 pages        = "272--286",
 doi          = "10.1007/978-3-540-72788-0\_26",
)
@inproceedings(03-een-extensible,
 author       = "Niklas E{\'e}n and Niklas S{\"o}rensson",
 year         = "2003",
 title        = "An Extensible SAT-solver",
 booktitle    = "SAT '03",
 series       = "LNCS",
 volume       = "2919",
 publisher    = "Springer",
 pages        = "502--518",
 doi          = "10.1007/978-3-540-24605-3\_37",
)
@inproceedings(11-fox-blasting,
 author       = "Anthony Fox",
 year         = "2011",
 title        = "{LCF}-Style Bit-Blasting in {HOL4}",
 booktitle    = "ITP '11",
 series       = "LNCS",
 publisher    = "Springer",
 pages        = "357--362",
 doi          = "10.1007/978-3-642-22863-6\_26",
)
@book(79-milner-lcf,
 author       = "Michael J. Gordon and Arthur J. Milner and Christopher P. Wadsworth",
 year         = "1979",
 title        = "Edinburgh {LCF}: A Mechanized Logic of Computation",
 series       = "LNCS",
 volume       = "78",
 publisher    = "Springer",
 doi          = "10.1007/3-540-09724-4",
)
@inproceedings(09-greve-quantifiers,
 author       = "David Greve",
 year         = "2009",
 title        = "Automated Reasoning with Quantified Formulae",
 booktitle    = "ACL2 '09",
 publisher    = "ACM",
 pages        = "110--113",
 doi          = "10.1145/1637837.1637855",
)
@inproceedings(05-hunt-meta,
 author       = "Warren A. {Hunt, Jr.} and Matt Kaufmann and Robert Bellarmine Krug and J Moore and Eric Whitman Smith",
 year         = "2005",
 title        = "Meta Reasoning in {ACL2}",
 booktitle    = "TPHOLs '05",
 series       = "LNCS",
 volume       = "3603",
 publisher    = "Springer",
 pages        = "163--178",
 doi          = "10.1007/11541868\_11",
)
@incollection(10-hardin-centaur,
 author       = "Warren A. {Hunt, Jr.} and Sol Swords and Jared Davis and Anna Slobodov\'{a}",
 year         = "2010",
 title        = "Use of Formal Verification at {Centaur} {Technology}",
 editor       = "David Hardin",
 booktitle    = "Design and Verification of Microprocessor Systems for High-Assurance Applications",
 publisher    = "Springer",
 pages        = "65--88",
 doi          = "10.1007/978-1-4419-1539-9\_3",
)
@inproceedings(11-kaufmann-defattach,
 author       = "Matt Kaufmann and J Strother Moore",
 year         = "2011",
 title        = "How Can I Do That with {ACL2}? Recent Enhancements to {ACL2}",
 booktitle    = "ACL2 '11",
 pages        = "46--60",
 doi          = "10.4204/EPTCS.70.4",
)
@article(09-maric-verified-sat,
 author       = "Filip Mari\'{c}",
 year         = "2009",
 title        = "Formalization and Implementation of Modern {SAT} Solvers",
 journal      = "Journal of Automated Reasoning",
 volume       = "43",
 number       = "1",
 pages        = "81--119",
 doi          = "10.1007/s10817-009-9127-8",
)
@inproceedings(08-mischenko-scalable,
 author       = "Alan Mishchenko and Michael Case and Robert Brayton and Stephen Jang",
 year         = "2008",
 title        = "Scalable and scalably-verifiable sequential synthesis",
 booktitle    = "ICCAD '08",
 publisher    = "IEEE",
 pages        = "234--241",
 doi          = "10.1109/ICCAD.2008.4681580",
)
@inproceedings(06-mishchenko-rewriting,
 author       = "Alan Mishchenko and Satrajit Chatterjee and Robert Brayton",
 year         = "2006",
 title        = "{DAG}-Aware {AIG} Rewriting: A Fresh Look at Combinational Logic Synthesis",
 booktitle    = "DAC '06",
 publisher    = "ACM",
 pages        = "532--535",
 doi          = "10.1145/1146909.1147048",
)
@techreport(05-mischenko-fraigs,
 author       = "Alan Mishchenko and Satrajit Chatterjee and Roland Jiang and Robert Brayton",
 year         = "2005",
 title        = "{FRAIG}s: A Unifying Representation for Logic Synthesis and Verification",
 type         = "Technical Report",
 institution  = "EECS Dept., UC Berkeley",
)
@inproceedings(12-oe-versat,
 author       = "Duckki Oe and Aaron Stump and Corey Oliver and Kevin Clancy",
 year         = "2012",
 title        = "{versat}: A Verified Modern SAT Solver",
 booktitle    = "VMCAI '12",
 series       = "LNCS",
 volume       = "7148",
 publisher    = "Springer",
 pages        = "363--378",
 doi          = "10.1007/978-3-642-27940-9\_24",
)
@inproceedings(11-swords-gl,
 author       = "Sol Swords and Jared Davis",
 year         = "2011",
 title        = "Bit-Blasting {ACL2} Theorems",
 booktitle    = "ACL2 '11",
 series       = "Electronic Proceedings in Theoretical Computer Science",
 volume       = "70",
 pages        = "84--102",
 doi          = "10.4204/EPTCS.70.7",
)
@incollection(10-swords-bddify,
 author       = "Sol Swords and Warren A. {Hunt, Jr.}",
 year         = "2010",
 title        = "A Mechanically Verified {AIG to BDD} Conversion Algorithm",
 booktitle    = "ITP '10",
 series       = "LNCS",
 volume       = "6172",
 publisher    = "Springer",
 pages        = "435--449",
 doi          = "10.1007/978-3-642-14052-5\_30",
)
@article(68-tseitin-propositional,
 author       = "G. S. Tseitin",
 year         = "1968",
 title        = "On the Complexity of Derivation in Propositional Calculus",
 journal      = "Zapiski nauchnykh seminarov LOMI",
 volume       = "8",
 pages        = "234--259",
 doi          = "10.1007/978-3-642-81955-1\_28",
 note         = "English translation of this volume: Consultants Bureau, N.Y., 1970, pp. 115--125",
)
@article(09-weber-sat,
 author       = "Tjark Weber and Hasan Amjad",
 year         = "2009",
 title        = "Efficiently Checking Propositional Refutations in {HOL} Theorem Provers",
 journal      = "Journal of Applied Logic",
 volume       = "7",
 number       = "1",
 pages        = "26--40",
 doi          = "10.1016/j.jal.2007.07.003",
)
@inproceedings(13-wetzler-sat,
 author       = "Nathan Wetzler and Marijn J. H. Heule and Warren A. {Hunt, Jr.}",
 year         = "2013",
 title        = "Mechanical Verification of {SAT} Refutations with Extended Resolution",
 booktitle    = "To appear in ITP 2013",
)