@inproceedings(Abrial06,
 author       = {J.-R. Abrial and M. Butler and S. Hallerstede and L. Voisin},
 year         = {2006},
 title        = {An Open Extensible Tool Environment for Event-b},
 booktitle    = {8th Int'l. Conf. Formal Methods and Software Engineering},
 publisher    = {Springer},
 pages        = {588--605},
 doi          = {10.1007/11901433\_32},
)
@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},
)
@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(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},
)
@techreport(Gamboa97,
 author       = {R.A. Gamboa},
 year         = {1997},
 title        = {Square Roots in ACL2: A Study in Sonata Form},
 type         = {Technical Report},
 institution  = {University of Texas at Austin},
 url          = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.4803},
)
@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},
)
@phdthesis(Harutunian07,
 author       = {Shant Harutunian},
 year         = {2007},
 title        = {Formal Verification of Computer Controlled Systems},
 school       = {University of Texas, Austin},
 url          = {https://www.lib.utexas.edu/etd/d/2007/harutunians68792/harutunians68792.pdf},
)
@incollection(Immler14,
 author       = {F. Immler},
 year         = {2014},
 title        = {Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations},
 booktitle    = {NASA Formal Methods},
 series       = {LNCS},
 volume       = {8430},
 publisher    = {Springer},
 pages        = {113--127},
 doi          = {10.1007/978-3-319-06200-6\_9},
)
@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},
)
@inproceedings(Rustan12,
 author       = {K. Leino and Rustan M.},
 year         = {2012},
 title        = {Automating Induction with an {SMT} Solver},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation},
 series       = {LNCS},
 volume       = {7148},
 publisher    = {Springer},
 pages        = {315--331},
 doi          = {10.1007/978-3-642-27940-9\_21},
)
@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},
)
@misc(DPLLproof,
 author       = {Y. Peng},
 year         = {2015},
 title        = {{Global convergence proof for a digital Phase-Locked Loop}},
 howpublished = {\url{https://bitbucket.org/pennyan/smtlink/src/7fdd38280be9e492a96947019f9b0c8cf10b3d91/examples/DPLL/DPLL_proof.lisp?at=master}},
 note         = {[Online; accessed 17-August-2015]},
)
@incollection(Peng15a,
 author       = {Y. Peng and M. Greenstreet},
 year         = {2015},
 title        = {Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification},
 booktitle    = {NASA Formal Methods},
 series       = {LNCS},
 volume       = {9058},
 publisher    = {Springer},
 pages        = {310--326},
 doi          = {10.1007/978-3-319-17524-9\_22},
)
@inproceedings(Reeber06,
 author       = {E. Reeber and {Hunt Jr.}, W.A.},
 year         = {2006},
 title        = {A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)},
 booktitle    = {Automated Reasoning},
 series       = {LNCS},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {453--467},
 doi          = {10.1007/11814771\_38},
)
@phdthesis(srinivasan2007,
 author       = {S.K. Srinivasan},
 year         = {2007},
 title        = {{Efficient Verification of Bit-level Pipelined Machines Using Refinement}},
 school       = {Georgia Institute of Technology},
)
@inproceedings(Swords11,
 author       = {S. Swords and J. Davis},
 year         = {2011},
 title        = {Bit-Blasting {ACL2} Theorems},
 booktitle    = {10\textsuperscript{th} Int'l. Workshop on the {ACL2} Theorem Prover and its Applications},
 pages        = {84--102},
 doi          = {10.4204/EPTCS.70.7},
)
@article(Weiser:1999:CSC:329124.329126,
 author       = {M. Weiser},
 year         = {1999},
 title        = {The Computer for the 21st Century},
 journal      = {SIGMOBILE Mob. Comput. Commun. Rev.},
 volume       = {3},
 number       = {3},
 pages        = {3--11},
 doi          = {10.1145/329124.329126},
)