@article(BBFF:JAR2020,
 author       = {Haniel Barbosa and Jasmin C. Blanchette and Mathias Fleury and Pascal Fontaine},
 year         = {2020},
 title        = {Scalable Fine-Grained Proofs for Formula Processing},
 journal      = {J. of Autom. Reason.},
 volume       = {64},
 number       = {3},
 pages        = {485--550},
 doi          = {10.1007/s10817-018-09502-y},
)
@inproceedings(BdM:IWIL2008,
 author       = {Bj{\o}rner, Nikolaj and {de Moura}, Leonardo},
 year         = {2008},
 title        = {Proofs and refutations, and {Z}3},
 booktitle    = {IWIL-7},
 series       = {CEUR},
 volume       = {418},
 pages        = {123--132},
)
@inproceedings(BGLMB:SMT2018,
 author       = {Fran\c{c}ois Bobot and Graham-Lengrand, St{\'e}phane and Bruno Marre and Guillaume Bury},
 year         = {2018},
 title        = {Centralizing equality reasoning in {MCSAT}},
 booktitle    = {SMT-16},
)
@article(MPB:JSC:1996:mcd,
 author       = {Maria Paola Bonacina},
 year         = {1996},
 title        = {On the reconstruction of proofs in distributed theorem proving: a modified {C}lause-{D}iffusion method},
 journal      = {J. of Symb. Comput.},
 volume       = {21},
 number       = {4--6},
 pages        = {507--522},
 doi          = {10.1006/jsco.1996.0028},
)
@inproceedings(MPB:AFM-NFM2017:conflictres,
 author       = {Maria Paola Bonacina},
 year         = {2018},
 title        = {On conflict-driven reasoning},
 booktitle    = {AFM-6},
 series       = {Kalpa Publications},
 volume       = {5},
 publisher    = {EasyChair},
 pages        = {31--49},
 doi          = {10.29007/spwm},
)
@incollection(MPB:PCRHandbook:2018:PTP,
 author       = {Maria Paola Bonacina},
 year         = {2018},
 title        = {Parallel theorem proving},
 booktitle    = {Handbook of Parallel Constraint Reasoning},
 chapter      = {6},
 publisher    = {Springer},
 pages        = {179--235},
 doi          = {10.1007/978-3-319-63516-3_6},
)
@incollection(MPB-PF-CR-CT:LNAI:2019:BeyondES,
 author       = {Maria Paola Bonacina and Pascal Fontaine and Christophe Ringeissen and Cesare Tinelli},
 year         = {2019},
 title        = {Theory combination: beyond equality sharing},
 booktitle    = {Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader},
 series       = {LNAI},
 volume       = {11560},
 publisher    = {Springer},
 pages        = {57--89},
 doi          = {10.1007/978-3-030-22102-7_3},
)
@inproceedings(MPB-SGL-NS:CADE2017:CDSAT,
 author       = {Maria Paola Bonacina and Graham-Lengrand, St{\'e}phane and Natarajan Shankar},
 year         = {2017},
 title        = {Satisfiability modulo theories and assignments},
 booktitle    = {CADE-26},
 series       = {LNAI},
 volume       = {10395},
 publisher    = {Springer},
 pages        = {42--59},
 doi          = {10.1007/978-3-319-63046-5_4},
)
@inproceedings(MPB-SGL-NS:CPP2018:CDSAText,
 author       = {Maria Paola Bonacina and Graham-Lengrand, St{\'e}phane and Natarajan Shankar},
 year         = {2018},
 title        = {Proofs in conflict-driven theory combination},
 booktitle    = {CPP-7},
 publisher    = {ACM},
 pages        = {186--200},
 doi          = {10.1145/3167096},
)
@article(MPB-SGL-NS:JAR:2019:CDSATtransition,
 author       = {Maria Paola Bonacina and Graham-Lengrand, St{\'e}phane and Natarajan Shankar},
 year         = {2020},
 title        = {Conflict-driven satisfiability for theory combination: transition system and completeness},
 journal      = {J. of Autom. Reason.},
 volume       = {64},
 number       = {3},
 pages        = {579--609},
 doi          = {10.1007/s10817-018-09510-y},
)
@article(MPB-SGL-NS:JAR:CDSAText,
 author       = {Maria Paola Bonacina and Graham-Lengrand, St{\'e}phane and Natarajan Shankar},
 year         = {2021},
 title        = {Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs},
 journal      = {J. of Autom. Reason.},
 volume       = {Submitted},
 pages        = {1--54},
 note         = {\url{http://profs.sci.univr.it/~bonacina/cdsat.html}},
)
@article(MPB-MKJ:JAR:2015:interpolationGround,
 author       = {Maria Paola Bonacina and Moa Johansson},
 year         = {2015},
 title        = {Interpolation systems for ground proofs in automated deduction: a survey},
 journal      = {J. of Autom. Reason.},
 volume       = {54},
 number       = {4},
 pages        = {353--390},
 doi          = {10.1007/s10817-015-9325-5},
)
@inproceedings(BKKM:FroCoS2019,
 author       = {Brau{\ss}e, Franz and Konstantin Korovin and Margarita Korovina and Norbert M{\"u}ller},
 year         = {2019},
 title        = {A {CDCL}-style calculus for solving non-linear constraints},
 booktitle    = {FroCoS-12},
 series       = {LNAI},
 volume       = {11715},
 publisher    = {Springer},
 pages        = {131--148},
 doi          = {10.1007/978-3-030-29007-8_8},
)
@inproceedings(CHHKS:CADE2017:RAT,
 author       = {Cruz-Felipe, Lu{\'{\i}}s and {Marijn J. H.} Heule and {Hunt Jr.}, {Warren A.} and Matt Kaufmann and Schneider-Kamp, Peter},
 year         = {2017},
 title        = {Efficient certified {RAT} verification},
 booktitle    = {CADE-26},
 series       = {LNAI},
 volume       = {10395},
 publisher    = {Springer},
 pages        = {220--236},
 doi          = {10.1007/978-3-319-63046-5_14},
)
@inproceedings(dMJ:VMCAI2013,
 author       = {{de Moura}, Leonardo and Dejan Jovanovi{\'c}},
 year         = {2013},
 title        = {A model-constructing satisfiability calculus},
 booktitle    = {VMCAI-14},
 series       = {LNCS},
 volume       = {7737},
 publisher    = {Springer},
 pages        = {1--12},
 doi          = {10.1007/978-3-642-35873-9_1},
)
@inproceedings(dMP:ADDCT2013,
 author       = {{de Moura}, Leonardo and Grant Olney Passmore},
 year         = {2013},
 title        = {Exact global optimization on demand (Presentation only)},
 booktitle    = {ADDCT-3},
 note         = {Available at \url{https://userpages.uni-koblenz.de/~sofronie/addct-2013/}},
)
@inproceedings(FMMNT:TACAS:2006,
 author       = {Pascal Fontaine and Jean-Yves Marion and Stephan Merz and Leonor Prensa Nieto and Alwen Tiu},
 year         = {2006},
 title        = {Expressiveness+automation+soundness: towards combining {SMT} solvers and interactive proof assistants},
 booktitle    = {TACAS-12},
 series       = {LNCS},
 volume       = {3920},
 publisher    = {Springer},
 pages        = {167--181},
 doi          = {10.1007/11691372_11},
)
@inproceedings(SGL-DJ-BD:IJCAR2020,
 author       = {Graham-Lengrand, St{\'e}phane and Dejan Jovanovi{\'c} and Bruno Dutertre},
 year         = {2020},
 title        = {Solving bitvectors with {MCSAT}: explanations from bits and pieces},
 booktitle    = {IJCAR-10},
 series       = {LNAI},
 volume       = {12166},
 publisher    = {Springer},
 pages        = {103--121},
 doi          = {10.1007/978-3-030-51074-9_7},
)
@inproceedings(J:VMCAI2017,
 author       = {Dejan Jovanovi{\'c}},
 year         = {2017},
 title        = {Solving nonlinear integer arithmetic with {MCSAT}},
 booktitle    = {VMCAI-18},
 series       = {LNCS},
 volume       = {10145},
 publisher    = {Springer},
 pages        = {330--346},
 doi          = {10.1007/978-3-319-52234-0_18},
)
@inproceedings(JBdM:FMCAD2013,
 author       = {Dejan Jovanovi{\'c} and Clark Barrett and Leonardo de Moura},
 year         = {2013},
 title        = {The design and implementation of the model-constructing satisfiability calculus},
 booktitle    = {FMCAD-13},
 publisher    = {ACM and IEEE},
)
@article(JdM:JAR:2013,
 author       = {Dejan Jovanovi{\'c} and {de Moura}, Leonardo},
 year         = {2013},
 title        = {Cutting to the chase: solving linear integer arithmetic},
 journal      = {J. of Autom. Reason.},
 volume       = {51},
 pages        = {79--108},
 doi          = {10.1007/s10817-013-9281-x},
)
@inproceedings(JdM:IJCAR2012,
 author       = {Dejan Jovanovi{\'c} and Leonardo de Moura},
 year         = {2012},
 title        = {Solving non-linear arithmetic},
 booktitle    = {IJCAR-6},
 series       = {LNAI},
 volume       = {7364},
 publisher    = {Springer},
 pages        = {339--354},
 doi          = {10.1007/978-3-642-31365-3_27},
)
@inproceedings(KBTRH:FMCAD2016,
 author       = {Guy Katz and Clark W. Barrett and Cesare Tinelli and Andrew Reynolds and Liana Hadarean},
 year         = {2016},
 title        = {Lazy proofs for {DPLL}({T})-based {SMT} solvers},
 booktitle    = {FMCAD-16},
 publisher    = {ACM and IEEE},
 pages        = {93--100},
 doi          = {10.1109/FMCAD.2016.7886666},
)
@incollection(Nelson:1983,
 author       = {Greg Nelson},
 year         = {1983},
 title        = {Combining satisfiability procedures by equality sharing},
 booktitle    = {Automatic Theorem Proving: After 25 Years},
 publisher    = {AMS},
 pages        = {201--211},
 doi          = {10.1090/conm/029/11},
)
@article(NelsonOppen:TOPLAS:1979,
 author       = {Greg Nelson and Derek C. Oppen},
 year         = {1979},
 title        = {Simplification by Cooperating Decision Procedures},
 journal      = {ACM Trans. on Prog. Lang. and Syst.},
 volume       = {1},
 number       = {2},
 pages        = {245--257},
 doi          = {10.1145/357073.357079},
)
@article(ShankarSurvey:2009,
 author       = {Natarajan Shankar},
 year         = {2009},
 title        = {Automated deduction for verification},
 journal      = {ACM Comput. Surv.},
 volume       = {41},
 number       = {4},
 pages        = {507--522},
 doi          = {10.1145/1592434.1592437},
)
@inproceedings(ZWR:SAT2016,
 author       = {Aleksandar Zelji{\'{c}} and Christoph M. Wintersteiger and Philipp R{\"u}mmer},
 year         = {2016},
 title        = {Deciding bit-vector formulas with {\tt mc}{{\tt SAT}}},
 booktitle    = {SAT-19},
 series       = {LNCS},
 volume       = {9710},
 publisher    = {Springer},
 pages        = {249--266},
 doi          = {10.1007/978-3-319-40970-2_16},
)
@inproceedings(ZhangMalik:DATE2003,
 author       = {Lintao Zhang and Sharad Malik},
 year         = {2003},
 title        = {Validating {SAT} solvers using an independent resolution-based checker: practical implementations and other applications},
 booktitle    = {DATE 2003},
 publisher    = {IEEE},
 pages        = {10880--10885},
 doi          = {10.5555/789083.1022835},
)