@inproceedings(armand-et-al-2011,
 author       = {Micha{\"e}l Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Th{\'e}ry and Benjamin Werner},
 year         = {2011},
 title        = {A Modular Integration of {SAT}/\penalty\exhyphenpenalty {SMT} Solvers to {Coq} through Proof Witnesses},
 editor       = {Jean-Pierre Jouannaud and Zhong Shao},
 booktitle    = {CPP~2011},
 series       = {LNCS},
 volume       = {7086},
 publisher    = {Springer},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@article(barbosa-2019,
 author       = {Haniel Barbosa and Jasmin~C. Blanchette and Mathias Fleury and Pascal Fontaine},
 year         = {2019},
 title        = {Scalable Fine-Grained Proofs for Formula Processing},
 journal      = {Journal of Automated Reasoning},
 doi          = {10.1007/s10817-018-09502-y},
)
@inproceedings(aitp19,
 author       = {Haniel Barbosa and Jasmin~C. Blanchette and Mathias Fleury and Pascal Fontaine and Hans-J\IeC{\"o}rg Schurr},
 year         = {2019},
 title        = {Better {SMT} proofs for easier reconstruction},
 editor       = {Thomas~C. Hales and Cezary Kaliszyk and Ramana Kumar and Stephan Schulz and Josef Urban},
 booktitle    = {{AITP} 2019},
)
@misc(SMTLIB,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2016},
 title        = {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
 howpublished = {\url{www.SMT-LIB.org}},
)
@incollection(barrett-2009,
 author       = {Clark Barrett and Roberto Sebastiani and Sanjit Seshia and Cesare Tinelli},
 year         = {2009},
 title        = {Satisfiability Modulo Theories},
 editor       = {Armin Biere and Marijn J.~H. Heule and Hans van Maaren and Toby Walsh},
 booktitle    = {Handbook of Satisfiability},
 chapter      = {26},
 series       = {Frontiers in Artificial Intelligence and Applications},
 volume       = {185},
 publisher    = {IOS Press},
 pages        = {825--885},
)
@inproceedings(besson-2011,
 author       = {Fr{\'e}d{\'e}ric Besson and Pascal Fontaine and Laurent Th{\'e}ry},
 year         = {2011},
 title        = {A Flexible Proof Format for {SMT}: A Proposal},
 editor       = {Pascal Fontaine and Aaron Stump},
 booktitle    = {PxTP 2011},
 pages        = {15--26},
 url          = {https://hal.inria.fr/hal-00642544/},
)
@article(Blanchette2016-isar,
 author       = {Jasmin~C. Blanchette and Sascha B{\"{o}}hme and Mathias Fleury and Steffen~J. Smolka and Albert Steckermeier},
 year         = {2016},
 title        = {Semi-intelligible {I}sar Proofs from Machine-Generated Proofs},
 journal      = {Journal of Automated Reasoning},
 volume       = {56},
 number       = {2},
 pages        = {155--200},
 doi          = {10.1007/s10817-015-9335-3},
)
@inproceedings(bohme-2010,
 author       = {Sascha B{\"o}hme and Tjark Weber},
 year         = {2010},
 title        = {Fast LCF-Style Proof Reconstruction for Z3},
 editor       = {Matt Kaufmann and Lawrence~C. Paulson},
 booktitle    = {ITP 2010},
 series       = {LNCS},
 volume       = {6172},
 publisher    = {Springer},
 pages        = {179--194},
 doi          = {10.1007/978-3-642-14052-5\_14},
)
@inproceedings(verit,
 author       = {Thomas Bouton and Diego C.~B. de~Oliveira and David D{\'{e}}harbe and Pascal Fontaine},
 year         = {2009},
 title        = {{veriT}: An Open, Trustable and Efficient {SMT}-solver},
 editor       = {Renate~A. Schmidt},
 booktitle    = {CADE 2009},
 series       = {LNCS},
 volume       = {5663},
 publisher    = {Springer},
 pages        = {151--156},
 doi          = {10.1007/978-3-642-02959-2\_12},
)
@inproceedings(DBLP:conf/cc/BuchwaldLU16,
 author       = {Sebastian Buchwald and Denis Lohner and Sebastian Ullrich},
 year         = {2016},
 title        = {Verified construction of static single assignment form},
 booktitle    = {{CC}},
 publisher    = {{ACM}},
 pages        = {67--76},
 doi          = {10.1145/2892208.2892211},
)
@inproceedings(deharbe-2011,
 author       = {David D{\'e}harbe and Pascal Fontaine and Woltzenlogel~Paleo, Bruno},
 year         = {2011},
 title        = {Quantifier Inference Rules for {SMT} Proofs},
 editor       = {Pascal Fontaine and Aaron Stump},
 booktitle    = {PxTP 2011},
 pages        = {33--39},
 url          = {https://hal.inria.fr/hal-00642535},
)
@inproceedings(EkiciKKMRT16,
 author       = {Burak Ekici and Guy Katz and Chantal Keller and Alain Mebsout and Andrew~J. Reynolds and Cesare Tinelli},
 year         = {2016},
 title        = {Extending {SMTCoq}, a Certified Checker for {SMT} (Extended Abstract)},
 editor       = {Jasmin~C. Blanchette and Cezary Kaliszyk},
 booktitle    = {HaTT 2016},
 series       = {{EPTCS}},
 volume       = {210},
 pages        = {21--29},
 doi          = {10.4204/EPTCS.210.5},
)
@article(McLaughlinBG06,
 author       = {Sean McLaughlin and Clark Barrett and Yeting Ge},
 year         = {2006},
 title        = {Cooperating Theorem Provers: {A} Case Study Combining {HOL-Light} and {CVC} {L}ite},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {144},
 number       = {2},
 pages        = {43--51},
 doi          = {10.1016/j.entcs.2005.12.005},
)
@inproceedings(Z3,
 author       = {Leonardo de~Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {Z3: An Efficient {SMT} Solver},
 editor       = {C.~R. Ramakrishnan and Jakob Rehof},
 booktitle    = {TACAS 2008},
 series       = {LNCS},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@article(Ordered_Resolution_Prover-AFP,
 author       = {Anders Schlichtkrull and Jasmin~C. Blanchette and Dmitriy Traytel and Uwe Waldmann},
 year         = {2018},
 title        = {Formalization of Bachmair and Ganzinger's Ordered Resolution Prover},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Ordered_Resolution_Prover.html}, Formal proof development},
)
@inproceedings(DBLP:conf/cade/SchlichtkrullBT18,
 author       = {Anders Schlichtkrull and Jasmin~C. Blanchette and Dmitriy Traytel and Uwe Waldmann},
 year         = {2018},
 title        = {Formalizing Bachmair and Ganzinger's Ordered Resolution Prover},
 booktitle    = {{IJCAR}},
 series       = {LNCS},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {89--107},
 doi          = {10.1007/978-3-319-94205-6\_7},
)
@book(DBLP:books/daglib/0090562,
 author       = {Alexander Schrijver},
 year         = {1999},
 title        = {Theory of Linear and Integer Programming},
 series       = {Wiley - Interscience Series in Discrete Mathematics and Optimization},
 publisher    = {Wiley},
)
@article(Stump-2013,
 author       = {Aaron Stump and Duckki Oe and Andrew Reynolds and Liana Hadarean and Cesare Tinelli},
 year         = {2013},
 title        = {SMT Proof Checking Using a Logical Framework},
 journal      = {Formal Methods in System Design},
 volume       = {42},
 number       = {1},
 pages        = {91--118},
 doi          = {10.1007/s10703-012-0163-3},
)
@article(Formal_SSA-AFP,
 author       = {Sebastian Ullrich and Denis Lohner},
 year         = {2016},
 title        = {Verified Construction of Static Single Assignment Form},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Formal_SSA.html}, Formal proof development},
)