@inproceedings(Armand2011,
 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    = {Certified Programs and Proofs},
 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(Barrett2011,
 author       = {Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovi{\'{c}} and Tim King and Andrew Reynolds and Cesare Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {Computer Aided Verification (CAV)},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1_14},
)
@article(barrett-2015,
 author       = {Clark Barrett and De Moura, Leonardo and Pascal Fontaine},
 year         = {2015},
 title        = {Proofs in satisfiability modulo theories},
 journal      = {All about proofs, Proofs for all},
 volume       = {55},
 number       = {1},
 pages        = {23--44},
)
@techreport(SMTLIB,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2017},
 title        = {{The SMT-LIB Standard: Version 2.6}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 note         = {Available at {\tt www.SMT-LIB.org}},
)
@incollection(Barrett2018,
 author       = {Clark W. Barrett and Cesare Tinelli},
 year         = {2018},
 title        = {Satisfiability Modulo Theories},
 editor       = {Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and Roderick Bloem},
 booktitle    = {Handbook of Model Checking.},
 publisher    = {Springer},
 pages        = {305--343},
 doi          = {10.1007/978-3-319-10575-8\_11},
)
@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},
)
@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 22},
 series       = {LNCS},
 volume       = {5663},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {151--156},
 doi          = {10.1007/978-3-642-02959-2\_12},
)
@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},
)
@article(Downey1980,
 author       = {Peter J. Downey and Ravi Sethi and Robert Endre Tarjan},
 year         = {1980},
 title        = {Variations on the Common Subexpression Problem},
 journal      = {J. ACM},
 volume       = {27},
 number       = {4},
 pages        = {758--771},
 doi          = {10.1145/322217.322228},
)
@inproceedings(SMTCoq,
 author       = {Burak Ekici and Alain Mebsout and Cesare Tinelli and Chantal Keller and Guy Katz and Andrew Reynolds and Clark Barrett},
 year         = {2017},
 title        = {{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into {C}oq},
 editor       = {Rupak Majumdar and Kun{\v{c}}ak, Viktor},
 booktitle    = {CAV 2017},
 series       = {LNCS},
 volume       = {10426},
 publisher    = {Springer},
 pages        = {126--133},
 doi          = {10.1007/978-3-319-63390-9\_7},
)
@inproceedings(fleury-2019,
 author       = {Mathias Fleury and Hans{-}J{\"{o}}rg Schurr},
 year         = {2019},
 title        = {Reconstructing {veriT} Proofs in {Isabelle/HOL}},
 editor       = {Giselle Reis and Haniel Barbosa},
 booktitle    = {PxTP 2019},
 series       = {{EPTCS}},
 volume       = {301},
 pages        = {36--50},
 doi          = {10.4204/EPTCS.301.6},
)
@article(Nelson1980,
 author       = {Greg Nelson and Derek C. Oppen},
 year         = {1980},
 title        = {{Fast Decision Procedures Based on Congruence Closure}},
 journal      = {J. ACM},
 volume       = {27},
 number       = {2},
 pages        = {356--364},
 doi          = {10.1145/322186.322198},
)
@inproceedings(schurr-2021,
 author       = {Hans-J\IeC{\"o}rg Schurr and Mathias Fleury and Martin Desharnais},
 year         = {2021},
 title        = {Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant},
 booktitle    = {CADE 28},
 series       = {LNCS},
)
@article(Stump2013,
 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},
)
@inproceedings(Sutcliffe2004,
 author       = {Geoff Sutcliffe and J{\"u}rgen Zimmer and Stephan Schulz},
 year         = {2004},
 title        = {{TSTP} Data-Exchange Formats for Automated Theorem Proving Tools},
 editor       = {Weixiong Zhang and Volker Sorge},
 booktitle    = {Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems},
 series       = {Frontiers in Artificial Intelligence and Applications},
 volume       = {112},
 publisher    = {IOS Press},
 pages        = {201--215},
)