@inproceedings(Armand11,
 author       = {M. Armand and G. Faure and B. Gr{\'e}goire and C. Keller and L. Th{\'e}ry and B. Werner},
 year         = {2011},
 title        = {A Modular Integration of SAT/SMT Solvers to Coq Through Proof Witnesses},
 booktitle    = {1st Int'l. Conf. Certified Programs and Proofs},
 publisher    = {Springer},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@incollection(Barrett04,
 author       = {C. Barrett and S. Berezin},
 year         = {2004},
 title        = {CVC Lite: A New Implementation of the Cooperating Validity Checker},
 booktitle    = {Computer Aided Verification},
 series       = {LNCS},
 volume       = {3114},
 publisher    = {Springer},
 pages        = {515--518},
 doi          = {10.1007/978-3-540-27813-9\_49},
)
@misc(Barrett10,
 author       = {C. Barrett and A. Stump and C. Tinelli},
 year         = {2010},
 title        = {{The SMT-LIB Standard: Version 2.0}},
 howpublished = {\url{http://www.cs.nyu.edu/~barrett/pubs/BST10.pdf}},
 note         = {[Online; accessed 17-August-2015]},
)
@inproceedings(Besson06,
 author       = {F. Besson},
 year         = {2007},
 title        = {Fast Reflexive Arithmetic Tactics the Linear Case and Beyond},
 booktitle    = {2006 Int'l. Conf. Types for Proofs and Programs},
 publisher    = {Springer},
 pages        = {48--62},
 doi          = {10.1007/978-3-540-74464-1\_4},
)
@article(Blanchette13,
 author       = {J.C. Blanchette and S. B\"{o}hme and L.C. Paulson},
 year         = {2013},
 title        = {Extending Sledgehammer with {SMT} Solvers},
 journal      = {J. Automated Reasoning},
 volume       = {51},
 number       = {1},
 pages        = {109--128},
 doi          = {10.1007/s10817-013-9278-5},
)
@article(Deharbe14,
 author       = {D. D{\'e}harbe and P. Fontaine and Y. Guyot and L. Voisin},
 year         = {2014},
 title        = {Integrating {SMT} Solvers in Rodin},
 journal      = {Sci. Comput. Program.},
 volume       = {94},
 number       = {P2},
 pages        = {130--143},
 doi          = {10.1016/j.scico.2014.04.012},
)
@phdthesis(Dill87,
 author       = {David L. Dill},
 year         = {1987},
 title        = {Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits},
 school       = {Carnegie Mellon University},
 address      = {Pittsburgh, PA, USA},
 url          = {http://reports-archive.adm.cs.cmu.edu/anon/scan/CMU-CS-88-119.pdf},
 note         = {AAI8814716},
)
@incollection(Dutertre2014,
 author       = {B. Dutertre},
 year         = {2014},
 title        = {Yices 2.2},
 booktitle    = {Computer Aided Verification},
 series       = {LNCS},
 volume       = {8559},
 publisher    = {Springer},
 pages        = {737--744},
 doi          = {10.1007/978-3-319-08867-9\_49},
)
@inproceedings(Burak17,
 author       = {Burak Ekici and Alain Mebsout and Cesare Tinelli and Chantal Keller and Guy Katz and Andrew Reynolds and Clark Barrett},
 year         = {2017},
 title        = {SMTCoq: A Plug-In for Integrating SMT Solvers into Coq},
 editor       = {Rupak Majumdar and Kun{\v{c}}ak, Viktor},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {126--133},
 doi          = {10.1007/978-3-319-63390-9_7},
)
@inproceedings(Erkok08,
 author       = {Levent Erk{\"{o}}k and John Matthews},
 year         = {2008},
 title        = {Using Yices as an Automated Solver in Isabelle/HOL},
 booktitle    = {In Automated Formal Methods’08},
 publisher    = {ACM Press},
 pages        = {3--13},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.8123},
)
@inproceedings(Fontaine06,
 author       = {P. Fontaine and J.-Y. Marion and S. Merz and L.P. Nieto and A. Tiu},
 year         = {2006},
 title        = {Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants},
 booktitle    = {12th Int'l. Conf. Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer},
 pages        = {167--181},
 doi          = {10.1007/11691372\_11},
)
@article(Harrison98,
 author       = {J. Harrison and L. Th{\'e}ry},
 year         = {1998},
 title        = {A Skeptic's Approach to Combining HOL and Maple},
 journal      = {J. Automated Reasoning},
 volume       = {21},
 number       = {3},
 pages        = {279--294},
 doi          = {10.1023/A:1006023127567},
)
@inproceedings(Cruz2017,
 author       = {Marijn Heule and Warren Hunt and Matt Kaufmann and Nathan Wetzler},
 year         = {2017},
 title        = {Efficient, Verified Checking of Propositional Proofs},
 editor       = {Ayala-Rinc{\'o}n, Mauricio and Mu{\~{n}}oz, C{\'e}sar A.},
 booktitle    = {Interactive Theorem Proving},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {269--284},
 doi          = {10.1007/978-3-319-66107-0_18},
)
@misc(Blanchette10,
 author       = {J. Blanchette, L. Paulson},
 year         = {2017},
 title        = {{Sledgehammer}},
 howpublished = {\url{https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf}},
 note         = {[Online; accessed 14-July-2018]},
)
@inproceedings(KaufmannS17,
 author       = {Matt Kaufmann and Sol Swords},
 year         = {2017},
 title        = {Meta-extract: Using Existing Facts in Meta-reasoning},
 editor       = {Slobodov{\'{a}} and Jr.},
 pages        = {47--60},
 doi          = {10.4204/EPTCS.249.4},
 url          = {http://arxiv.org/abs/1705.00766},
)
@incollection(Lahiri2004,
 author       = {S.K. Lahiri and S.A. Seshia},
 year         = {2004},
 title        = {The UCLID Decision Procedure},
 booktitle    = {Computer Aided Verification},
 series       = {LNCS},
 volume       = {3114},
 publisher    = {Springer},
 pages        = {475--478},
 doi          = {10.1007/978-3-540-27813-9\_40},
)
@article(Manolios2006,
 author       = {P. Manolios and S.K. Srinivasan},
 year         = {2006},
 title        = {A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures},
 journal      = {J. of Automated Reasoning},
 volume       = {37},
 number       = {1-2},
 pages        = {93--116},
 doi          = {10.1007/s10817-006-9035-0},
)
@inproceedings(Mclaughlin06,
 author       = {S. Mclaughlin and Cl. Barrett and Y. Ge},
 year         = {2006},
 title        = {Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite},
 booktitle    = {In Proc. 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning},
 series       = {ENTCS},
 volume       = {144(2)},
 publisher    = {Elsevier},
 pages        = {43--51},
 doi          = {10.1016/j.entcs.2005.12.005},
)
@inproceedings(Merz12,
 author       = {S. Merz and H. Vanzetto},
 year         = {2012},
 title        = {Automatic Verification of TLA$^{+}$; Proof Obligations with SMT Solvers},
 booktitle    = {18th Int'l. Conf. Logic for Programming, Artificial Intelligence, and Reasoning},
 publisher    = {Springer},
 pages        = {289--303},
 doi          = {10.1007/978-3-642-28717-6\_23},
)
@inproceedings(Moura08,
 author       = {Leonardo Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {Z3: {An} Efficient {SMT} Solver},
 editor       = {C.R. Ramakrishnan and Jakob Rehof},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@inproceedings(Moura15,
 author       = {Leonardo de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
 year         = {2015},
 title        = {The Lean Theorem Prover (System Description)},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {Automated Deduction - CADE-25},
 publisher    = {Springer International Publishing},
 pages        = {378--388},
 doi          = {10.1007/978-3-319-21401-6_26},
)
@inproceedings(Peng2015-acl2,
 author       = {Yan Peng and Mark Greenstreet},
 year         = {2015},
 title        = {Extending {ACL2} with {SMT} Solvers},
 editor       = {Matt Kaufmann and David L. Rager},
 booktitle    = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem Prover and Its Applications},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {192},
 publisher    = {Open Publishing Association},
 address      = {Austin, Texas, USA, 1--2 October 2015},
 pages        = {61--77},
 doi          = {10.4204/EPTCS.192.6},
)
@inproceedings(Peng2015-nfs,
 author       = {Yan Peng and Mark Greenstreet},
 year         = {2015},
 title        = {Integrating {SMT} with Theorem Proving for Analog/Mixed-Signal Circuit Verification},
 editor       = {Klaus Havelund and Gerard Holzmann and Rajeev Joshi},
 booktitle    = {NASA Formal Methods},
 publisher    = {Springer International Publishing},
 pages        = {310--326},
 doi          = {10.1007/978-3-319-17524-9_22},
)
@proceedings(DBLP:journals/corr/SlobodovaJ17,
 editor       = {Anna Slobodov{\'{a}} and Warren A. Hunt Jr.},
 year         = {2017},
 title        = {Proceedings 14th International Workshop on the {ACL2} Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017},
 series       = {{EPTCS}},
 volume       = {249},
 url          = {http://arxiv.org/abs/1705.00766},
)
@phdthesis(srinivasan2007,
 author       = {S.K. Srinivasan},
 year         = {2007},
 title        = {{Efficient Verification of Bit-level Pipelined Machines Using Refinement}},
 school       = {Georgia Institute of Technology},
 url          = {http://hdl.handle.net/1853/19815},
)
@article(Vazou:2017,
 author       = {Niki Vazou and Anish Tondwalkar and Vikraman Choudhury and Ryan G. Scott and Ryan R. Newton and Philip Wadler and Ranjit Jhala},
 year         = {2017},
 title        = {Refinement Reflection: Complete Verification with SMT},
 journal      = {Proc. ACM Program. Lang.},
 volume       = {2},
 number       = {POPL},
 pages        = {53:1--53:31},
 doi          = {10.1145/3158141},
)