SMTProofs.bib

@string{entcs  = "Electronic Notes in Theoretical Computer Science"}
@string{lncs   = "Lecture Notes in Computer Science"}
@string{lnai   = "Lecture Notes in Artificial Intelligence"}
@string{j-jucs = "Journal of Universal Computer Science"}
@string{tcs    = "Theoretical Computer Science"}
@string{jacm   = "Journal of the ACM"}
@string{jar    = "Journal of Automated Reasoning"}
@string{sigplan = "ACM SIG{\-}PLAN Notices"}

@string{acm   = "ACM press"}
@string{ieee  = "IEEE Computer Society"}
@string{springer  = "Springer"}

@string{cade   = "Proc. Conference on Automated Deduction (CADE)"}
@string{cav    = "Computer Aided Verification (CAV)"}
@string{cp     = "Principles and Practice of Constraint Programming
                 (CP)"}
@string{csl    = "Computer Science Logic (CSL)"}
@string{dac    = "Design Automation Conference (DAC)"}
@string{esop   = "European Symposium on Programming (ESOP)"}
@string{fmcad  = "Formal Methods In Computer-Aided Design (FMCAD)"}
@string{frocos = "Frontiers of Combining Systems ({FroCoS})"}
@string{iccad  = "{IEEE} International Conference on Computer-Aided
                 Design (ICCAD)"}
@string{ictac  = "International Conference on Theoretical
  Aspects of Computing (ICTAC)"}
@string{ifm    = "Integrated Formal Methods (IFM)"}
@string{ijcar  = "International Joint Conference on Automated Reasoning
                 (IJCAR)"}
@string{jelia  = "Proc. European Conference Logics in Artificial Intelligence (JELIA)"}
@string{lics   = "Logic In Computer Science (LICS)"}
@string{lpar   = "Logic for Programming, Artificial Intelligence, and
                  Reasoning (LPAR)"}
@string{pdpar  = "Pragmatics of Decision Procedures in Automated Reasoning
                  (PDPAR)"}
@string{smt    = "International Workshop on Satisfiability Modulo Theories (SMT)"}
@string{rta    = "Rewriting Techniques and Applications (RTA)"}
@string{tacas  = "Tools and Algorithms for Construction and Analysis of
                 Systems (TACAS)"}

@Misc{Barrett15,
  author       = "Clark Barrett and Aaron Stump and Cesare Tinelli",
  title        = "The {SMT-LIB} Standard : Version 2.0",
  month        = dec,
  year         = "2010",
}

@InCollection{Barrett14,
  author =       "Clark Barrett and Roberto Sebastiani and Sanjit A.
                 Seshia and Cesare Tinelli",
  title =        "Satisfiability Modulo Theories",
  chapter =      "26",
  pages =        "825--885",
  editor =       "Armin Biere and Marijn J. H. Heule and Hans van Maaren
                 and Toby Walsh",
  booktitle =    "Handbook of Satisfiability",
  publisher =    "IOS Press",
  year =         "2009",
  month =        feb,
  volume =       "185",
  ISBN =         "978-1-58603-929-5",
  ISSN =         "0922-6389",
  series =       "Frontiers in Artificial Intelligence and
                 Applications",
}

@article{Ge1,
  author    = "Yeting Ge and Clark Barrett and Cesare Tinelli",
  title     = "Solving Quantified Verification Conditions using Satisfiability Modulo Theories",
  journal   = "Annals of Mathematics and Artificial Intelligence",
  publisher = "Springer",
  volume    = 55,
  number    = "1-2",
  pages     = "101--122",
  month     = feb,
  year      = 2009,

}

@inproceedings{Ge2,
  author    = {Yeting Ge and
               Leonardo Mendon\c{c}a de Moura},
  title     = {Complete Instantiation for Quantified Formulas in Satisfiabiliby
               Modulo Theories},
  booktitle = {CAV},
  year      = {2009},
  pages     = {306-320},
  editor    = {Ahmed Bouajjani and
               Oded Maler},
  publisher = {Springer},
  series    = lncs,
  volume    = {5643},
  mysubject = "instantiation",
}


@inproceedings{Borralleras1,
  author    = {Cristina Borralleras and
               Salvador Lucas and
               Rafael Navarro-Marset and
               Enric Rodr\'{\i}guez-Carbonell and
               Albert Rubio},
  title     = {Solving Non-linear Polynomial Arithmetic via SAT Modulo
               Linear Arithmetic},
  booktitle = {CADE},
  year      = {2009},
  pages     = {294-305},
  ee        = {http://dx.doi.org/10.1007/978-3-642-02959-2_23},
  editor    = {Renate A. Schmidt},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
}

@Article{Nelson2,
  author       = "Greg Nelson and Derek C. Oppen",
  title        = "Fast Decision Procedures Based on Congruence Closure",
  journal      = jacm,
  volume       = "27",
  number       = "2",
  pages        = "356--364",
  year         = "1980",
  month        = apr,
  mysubject    = "combinations",
  mysubject    = "congruence",
}

@InProceedings{Moura9,
  author =       "Leonardo Mendon\c{c}a de Moura and Nikolaj
                 Bj{\o}rner",
  title =        "Efficient {E}-Matching for {SMT} Solvers",
  booktitle =    cade,
  year =         "2007",
  pages =        "183--198",
  editor =       "Frank Pfenning",
  publisher =    "Springer",
  series =       lncs,
  volume =       "4603",
  mysubject =    "instantiation",
}

@Article{Nieuwenhuis6,
  author =       "Robert Nieuwenhuis and Albert Oliveras",
  title =        "Fast congruence closure and extensions",
  journal =      "Information and Computation",
  volume =       "205",
  number =       "4",
  year =         "2007",
  pages =        "557--580",
  publisher =    "Academic Press, Inc.",
  address =      "Duluth, MN, USA",
}

@InProceedings{Dutertre1,
  title =        "{A Fast Linear-Arithmetic Solver for DPLL(T)}",
  author =       "Bruno Dutertre and Leonardo de Moura",
  booktitle =    cav,
  series =       lncs,
  pages =        "81--94",
  editors =      "T. Ball and R. B. Jones",
  volume =       "4144",
  publisher =    "Springer-Verlag",
  year =         "2006",
  mysubject    = "arithmetic",
}


@Article{Nelson3,
  author       = "Greg Nelson and Derek C. Oppen",
  title        = "Simplifications by Cooperating Decision Procedures",
  journal      = "ACM Transactions on Programming Languages and
                 Systems",
  volume       = "1",
  number       = "2",
  year         = "1979",
  pages        = "245--257",
  month        = oct,
  mysubject    = "combinations",
  mysubject    = "congruence",
}

@InProceedings{Tinelli1,
  author       = "Cesare Tinelli and Mehdi T.~Harandi",
  title        = "A new correctness proof of the {N}elson--{O}ppen
                 combination procedure",
  editor       = "F.~Baader and Klaus U.~Schulz",
  booktitle    = frocos,
  year         = "1996",
  month        = mar,
  publisher    = "Kluwer Academic Publishers",
  series       = "Applied Logic",
  pages        = "103--120",
  URL          = "citeseer.nj.nec.com/tinelli96new.html",
  mysubject    = "combinations",
}

@InProceedings{Bozzano6,
  author =       "Marco Bozzano and Roberto Bruttomesso and Alessandro
                 Cimatti and Tommi Junttila and Silvio Ranise and Peter
                 van Rossum and Roberto Sebastiani",
  booktitle =    cav,
  title =        "Efficient Satisfiability Modulo Theories via Delayed
                 Theory Combination",
  editor =       "Kousha Etessami and Sriram K. Rajamani",
  series =       lncs,
  volume =       "3576",
  year =         "2005",
  pages =        "335--349",
  publisher =    "Springer",
}

@inproceedings{SBD02,
  author    = "Aaron Stump and Clark W. Barrett and David L. Dill",
  title     = "{CVC}: A Cooperating Validity Checker",
  booktitle = "Proceedings of the $14^{th}$ International Conference on Computer Aided Verification (CAV '02)",
  series    = "Lecture Notes in Computer Science",
  volume    = 2404,
  publisher = "Springer-Verlag",
  editor    = "Ed Brinksma and Kim Guldstrand Larsen",
  pages     = "500--504",
  month     = jul,
  year      = 2002,
  note      = "Copenhagen, Denmark",
}

@inproceedings{BDL96,
  author    = "Clark W. Barrett and David L. Dill and Jeremy R. Levitt",
  title     = "Validity Checking for Combinations of Theories with Equality",
  booktitle = "Proceedings of the $1^{st}$ International Conference on Formal Methods In Computer-Aided Design (FMCAD '96)",
  series    = "Lecture Notes in Computer Science",
  volume    = 1166,
  publisher = "Springer-Verlag",
  editor    = "Mandayam Srivas and Albert Camilleri",
  pages     = "187--201",
  month     = nov,
  year      = 1996,
  note      = "Palo Alto, California",
}

@article{HHP93,
 author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon},
 title = {A Framework for Defining Logics},
 journal = {J. ACM},
 issue_date = {Jan. 1993},
 volume = {40},
 number = {1},
 month = jan,
 year = {1993},
 issn = {0004-5411},
 pages = {143--184},
 numpages = {42},
 url = {http://doi.acm.org/10.1145/138027.138060},
 doi = {10.1145/138027.138060},
 acmid = {138060},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {formal systems, interactive theorem proving, proof checking, typed lambda calculus},
}

@inproceedings{SBD02b,
   author = {Aaron Stump and Clark W. Barrett and David L. Dill},
   editor = {Frank Pfenning},
   title = {Producing Proofs from an Arithmetic Decision Procedure in
        Elliptical {LF}},
   booktitle = {Proceedings of the $3^{rd}$ International Workshop on
        Logical Frameworks and Meta-Languages (LFM '02)},
   series = {Electronic Notes in Theoretical Computer Science},
   volume = {70(2)},
   pages = {29--41},
   publisher = {Elsevier},
   month = jul,
   year = {2002},
   note = {Copenhagen, Denmark},
}

@incollection{SD02,
year={2002},
booktitle=cade,
volume={2392},
series={Lecture Notes in Computer Science},
editor={Voronkov, Andrei},
doi={10.1007/3-540-45620-1_32},
title={Faster Proof Checking in the Edinburgh Logical Framework},
publisher={Springer Berlin Heidelberg},
author={Stump, Aaron and Dill, David L.},
pages={392-407},
language={English}
}

@inproceedings{BDS02-CAV02,
  author    = "Clark W. Barrett and David L. Dill and Aaron Stump",
  title     = "Checking Satisfiability of First-Order Formulas by Incremental Translation to {SAT}",
  booktitle = "Proceedings of the $14^{th}$ International Conference on Computer Aided Verification (CAV '02)",
  series    = "Lecture Notes in Computer Science",
  volume    = 2404,
  publisher = "Springer-Verlag",
  editor    = "Ed Brinksma and Kim Guldstrand Larsen",
  pages     = "236--249",
  month     = jul,
  year      = 2002,
  note      = "Copenhagen, Denmark",
}

@Article{NieOT-JACM-06,
  author =       {Robert Nieuwenhuis and Albert Oliveras and Cesare
                  Tinelli},
  title =        {{Solving SAT and SAT Modulo Theories: from an
                  Abstract Davis-Putnam-Logemann-Loveland Procedure to
                  DPLL(T)}},
  journal =      {Journal of the ACM},
  year =         2006,
  volume =       53,
  number =       6,
  pages =        {937--977},
  month =        nov,
}

@incollection{FJO+03,
author = {Flanagan, Cormac and Joshi, Rajeev and Ou, Xinming and Saxe, James B.},
booktitle = {Computer Aided Verification},
doi = {10.1007/978-3-540-45069-6\_34},
editor = {Hunt, Warren A. and Somenzi, Fabio},
pages = {355--367},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Theorem Proving Using Lazy Proof Explication},
volume = {2725},
year = {2003}
}

@inproceedings{MBG06,
  author    = "Sean McLaughlin and Clark Barrett and Yeting Ge",
  title     = "Cooperating Theorem Provers: A Case Study Combining {HOL-L}ight and {CVC L}ite",
  booktitle = "Proceedings of the $3^{rd}$ Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05)",
  series    = "Electronic Notes in Theoretical Computer Science",
  volume    = "144(2)",
  publisher = "Elsevier",
  editor    = "Alessandro Armando and Alessandro Cimatti",
  pages     = "43--51",
  month     = jan,
  year      = 2006,
  note      = "Edinburgh, Scotland",
}

@inproceedings{BB04,
  author    = "Clark Barrett and Sergey Berezin",
  title     = "{CVC L}ite: A New Implementation of the Cooperating Validity Checker",
  booktitle = "Proceedings of the $16^{th}$ International Conference on Computer Aided Verification (CAV '04)",
  series    = "Lecture Notes in Computer Science",
  volume    = 3114,
  publisher = "Springer-Verlag",
  editor    = "Rajeev Alur and Doron A. Peled",
  pages     = "515--518",
  month     = jul,
  year      = 2004,
  note      = "Boston, Massachusetts",
}

@inproceedings{DR03,
author = {David Déharbe and Silvio Ranise},
booktitle = {First International Conference on Software Engineering and Formal Methods, 2003.},
isbn = {0-7695-1949-0},
pages = {220--228},
publisher = {IEEE},
shorttitle = {Software Engineering and Formal Methods, 2003.Proc},
title = {Light-weight theorem proving for debugging and verifying units of code},
year = {2003}
}

@incollection{FMM+06,
author = {Fontaine, Pascal and Marion, Jean-Yves and Merz, Stephan and Nieto, Leonor Prensa and Tiu, Alwen},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
editor = {Hermanns, Holger and Palsberg, Jens},
pages = {167--181},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Expressiveness + Automation + Soundness: Towards Combining {SMT} Solvers and Interactive Proof Assistants},
volume = {3920},
year = {2006}
}

@inproceedings{HCF+07,
address = {Bremen, Germany},
author = {Hurlin, Clément and Chaib, Amine and Fontaine, Pascal and Merz, Stephan and Weber, Tjark},
booktitle = {The Isabelle Workshop 2007 - Isabelle'07},
editor = {{Lucas Dixon}, Moa Johansson},
pages = {2--13},
title = {Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions},
year = {2007}
}

@incollection{H96,
year={1996},
booktitle={Formal Methods in Computer-Aided Design},
volume={1166},
series={Lecture Notes in Computer Science},
editor={Srivas, Mandayam and Camilleri, Albert},
title={HOL Light: A tutorial introduction},
publisher={Springer Berlin Heidelberg},
author={Harrison, John},
pages={265-269}
}

@book{NPW02,
  title={Isabelle/{HOL}: a proof assistant for higher-order logic},
  author={Nipkow, Tobias and Paulson, Lawrence C and Wenzel, Markus},
  volume={2283},
  year={2002},
  publisher={Springer}
}

@inproceedings{GB08,
author = {Ge, Yeting and Barrett, Clark},
booktitle = {Proceedings of the $6^{th}$ International Workshop on Satisfiability Modulo Theories (SMT '08)},
title = {Proof Translation and {SMT-LIB} Benchmark Certification: A Preliminary Report},
year = {2008}
}

@inproceedings{BT07,
  author    = "Clark Barrett and Cesare Tinelli",
  title     = "{CVC3}",
  booktitle = "Proceedings of the $19^{th}$ International Conference on Computer Aided Verification (CAV '07)",
  series    = "Lecture Notes in Computer Science",
  volume    = 4590,
  publisher = "Springer-Verlag",
  editor    = "Werner Damm and Holger Hermanns",
  pages     = "298--302",
  month     = jul,
  year      = 2007,
  note      = "Berlin, Germany",
}

@inproceedings{Z3,
 author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 title = {Z3: An Efficient SMT Solver},
 booktitle = {Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series = {TACAS'08/ETAPS'08},
 year = {2008},
 location = {Budapest, Hungary},
 pages = {337--340},
 numpages = {4},
}


@inproceedings{IsabelleZ3,
  author    = {Sascha B{\"o}hme},
  title     = {Proof Reconstruction for {Z3} in {Isabelle/HOL}},
  booktitle = {7th International Workshop on
               Satisfiability Modulo Theories (SMT '09)},
  year      = 2009
}

@inproceedings{iZ3,
 author = {McMillan, Kenneth L.},
 title = {Interpolants from Z3 Proofs},
 booktitle = {Proceedings of the International Conference on Formal Methods in Computer-Aided Design},
 series = {FMCAD '11},
 year = {2011},
 isbn = {978-0-9835678-1-3},
 location = {Austin, Texas},
 pages = {19--27},
 numpages = {9},
}

@incollection{M08,
author = {Moskal, Micha{\l}},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
editor = {Ramakrishnan, C R and Rehof, Jakob},
pages = {486--500},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {{Rocket-Fast} Proof Checking for {SMT} Solvers},
volume = {4963},
year = {2008}
}

@inproceedings{dMB08,
author = {de Moura, Leonardo and Bj{\o}rner, Nikolaj},
booktitle = {Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
title = {Proofs and Refutations, and {Z3}},
volume = {418},
year = {2008}
}

@incollection{BCF+08,
address = {Berlin, Heidelberg},
author = {Bruttomesso, Roberto and Cimatti, Alessandro and Franz\'{e}n, Anders and Griggio, Alberto and Sebastiani, Roberto},
booktitle = {Computer Aided Verification},
chapter = {28},
editor = {Gupta, Aarti and Malik, Sharad},
pages = {299--303},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {The {MathSAT} 4 {SMT} Solver},
volume = {5123},
year = {2008}
}

@incollection{BdOD+09,
author = {Bouton, Thomas and de Oliveira, Diego B. Caminha and Déharbe, David and Fontaine, Pascal},
booktitle = {Automated Deduction – CADE-22},
editor = {Schmidt, Renate A},
pages = {151--156},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {{veriT}: An Open, Trustable and Efficient {SMT}-Solver},
volume = {5663},
year = {2009}
}

@misc{lean,
author={Leonardo de Moura and Soonho Kong},
title={Lean theorem prover: \url{http://github.com/leanprover}},
year = {2014},
}

@PhdThesis{Passmore1,
  title =        "Combined Decision Procedures for Nonlinear
                 Arithmetics, Real and Complex",
  year =         "2011",
  author =       "Grant Olney Passmore",
  school =       "LFCS, School of Informatics, University of Edinburgh",
  mysubject =    "non-linear-arithmetic",
}
@InCollection{Bockmayr1,
  author       = "Alexander Bockmayr and V. Weispfenning",
  title        = "Solving numerical constraints",
  pages        = "751--842",
  chapter      = "12",
  volume       = "I",
  editor       = "John Alan Robinson and Andrei Voronkov",
  booktitle    = "Handbook of Automated Reasoning",
  publisher    = "Elsevier Science B.V.",
  year         = "2001",
  mysubject    = "arithmetic",
}

@InProceedings{Nieuwenhuis3,
  author       = "Robert Nieuwenhuis and Albert Oliveras",
  title        = "Union-Find and Congruence Closure Algorithms that Produce Proofs",
  booktitle    = pdpar,
  editor       = "Cesare Tinelli and Silvio Ranise",  
  year         = "2004",
}
@InProceedings{Bruttomesso4,
  title =        "The Open{SMT} Solver",
  author =       "Roberto Bruttomesso and Edgar Pek and Natasha
                 Sharygina and Aliaksei Tsitovich",
  booktitle =    "International Conference on Tools and Algorithms for
                 the Construction and Analysis of Systems (TACAS)",
  volume =       "6015",
  year =         "2010",
  pages =        "150--153",
  publisher =    "Springer",
  organization = "Springer",
  address =      "Paphos, Cyprus",
}
@InProceedings{Besson1,
  author       = "Frédéric Besson and Pascal Fontaine and Laurent Théry",
  title        = "A Flexible Proof Format for SMT: a Proposal",
  year         = "2011",
  booktitle =    "Workshop on Proof eXchange for Theorem Proving",
}

@InProceedings{Reynolds1,
title = "Comparing Proof Systems for Linear Real Arithmetic with {LFSC}",
author = "Andrew Reynolds and Liana Haderean and Cesare Tinelli and Yeting Ge and Aaron Stump and Clark Barrett",
booktitle = smt,
year = 2010
}

@inproceedings{SO08,
address = {New York, New York, USA},
author = {Stump, Aaron and Oe, Duckki},
booktitle = {Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning - SMT '08/BPR '08},
month = jul,
pages = {27},
publisher = {ACM Press},
title = {Towards an {SMT} proof format},
year = {2008}
}

@inproceedings{ORS09,
address = {New York, New York, USA},
author = {Oe, Duckki and Reynolds, Andrew and Stump, Aaron},
booktitle = {Proceedings of the 7th International Workshop on Satisfiability Modulo Theories - SMT '09},
month = aug,
pages = {6--13},
publisher = {ACM Press},
title = {Fast and flexible proof checking for {SMT}},
year = {2009}
}

@article{SOR+13,
author = {Stump, Aaron and Oe, Duckki and Reynolds, Andrew and Hadarean, Liana and Tinelli, Cesare},
journal = {Formal Methods in System Design},
month = jul,
number = {1},
pages = {91--118},
publisher = {Springer US},
title = {{SMT} proof checking using a logical framework},
volume = {42},
year = {2013}
}

@inproceedings{BFT11,
address = {Wroclaw, Pologne},
author = {Besson, Frédéric and Fontaine, Pascal and Théry, Laurent},
booktitle = {First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011},
month = aug,
title = {A Flexible Proof Format for {SMT}: a Proposal},
year = {2011}
}

@inproceedings{BW11,
address = {Wroclaw, Pologne},
author = {B\"{o}hme, Sascha and Weber, Tjark},
booktitle = {First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011},
month = aug,
title = {Designing Proof Formats: A User's Perspective --- Experience Report},
year = {2011}
}

@inproceedings{KBD13,
  author    = "Timothy King and Clark Barrett and Bruno Dutertre",
  title     = "Simplex with Sum of Infeasibilities for {SMT}",
  booktitle = "Proceedings of the $13^{th}$ International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)",
  publisher = "FMCAD Inc.",
  pages     = "189--196",
  month     = oct,
  year      = 2013,
  note      = "Portland, Oregon",
}

@inproceedings{Hofferek1,
author = {Georg Hofferek and Ashutosh Gupta and Bettina K\"{o}nighofer and Jie-Hong Roland Jiang and Roderick Paul Bloem},
title = {Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof},
booktitle = {FMCAD 2013 - Formal Methods in Computer-Aided Design},
year = {2013},
pages = {77 - 84},
publisher = {IEEE},
}

@inproceedings{Deharbe1,
year={2012},
isbn={978-3-642-30884-0},
booktitle={Abstract State Machines, Alloy, B, VDM, and Z},
volume={7316},
series={Lecture Notes in Computer Science},
editor={Derrick, John and Fitzgerald, John and Gnesi, Stefania and Khurshid, Sarfraz and Leuschel, Michael and Reeves, Steve and Riccobene, Elvinia},
doi={10.1007/978-3-642-30885-7_14},
title={SMT Solvers for Rodin},
url={http://dx.doi.org/10.1007/978-3-642-30885-7_14},
publisher={Springer Berlin Heidelberg},
author={Déharbe, David and Fontaine, Pascal and Guyot, Yoann and Voisin, Laurent},
pages={194-207}
}

@inproceedings{AFGKTW11b,
    hal_id = {hal-00639130},
    url = {http://hal.inria.fr/hal-00639130},
    title = {{A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses}},
    author = {Armand, Micha{\"e}l and Faure, Germain and Gr{\'e}goire, Benjamin and Keller, Chantal and Thery, Laurent and Werner, Benjamin},
    abstract = {{We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.}},
    language = {Anglais},
    affiliation = {MARELLE - INRIA Sophia Antipolis , TYPICAL - INRIA Saclay - Ile de France , Laboratoire d'informatique de l'{\'e}cole polytechnique - LIX},
    booktitle = {{CPP - Certified Programs and Proofs - First International Conference - 2011}},
    publisher = {Springer},
    pages = {135-150},
    address = {Kenting, Ta{\"\i}wan, Province De Chine},
    volume = {7086},
    editor = {Jouannaud, Jean-Pierre and Shao, Zhong },
    series = {Lecture notes in computer science - LNCS },
    audience = {internationale },
    doi = {10.1007/978-3-642-25379-9\_12 },
    year = {2011},
    month = Dec,
    pdf = {http://hal.inria.fr/hal-00639130/PDF/cpp11.pdf},
}

@PhdThesis{keller13,
  author =       {Keller, C.},
  title =        {{A Matter of Trust: Skeptical Communication Between Coq and External Provers}},
  school =       {École Polytechnique},
  year =         {2013},
  month =        {June}
}

@inproceedings{RTH11,
  Author =	 {Andrew Reynolds and Cesare Tinelli and Liana
                  Hadarean},
  Booktitle =	 {Proceedings of the 9th International Workshop on
                  Satisfiability Modulo Theories (Snowbird, USA)},
  Editor =	 {S.~Lahiri and S.~Seshia},
  Title =	 {Certified Interpolant Generation for {EUF}},
  Year =	 2011
}

@inproceedings{RHT+10,
  author    = "Andrew Reynolds and Liana Hadarean and Cesare Tinelli and Yeting Ge and Aaron Stump and Clark Barrett",
  title     = "Comparing Proof Systems for Linear Real Arithmetic with {LFSC}",
  booktitle = "Proceedings of the $8^{th}$ International Workshop on Satisfiability Modulo Theories (SMT '10)",
  month     = jul,
  year      = 2010,
  note      = "Edinburgh, Scotland",
}

@inproceedings{B13,
address = {Lake Placid, USA},
author = {Guillaume Burel},
booktitle = {Third International Workshop on Proof eXchange for Theorem Proving - PxTP 2013},
month = {june},
title = {A Shallow Embedding of Resolution and Superposition Proofs into the {$\lambda\Pi$}-Calculus Modulo},
year = {2013}
}





@inproceedings{B44, 
Author = {Joseph Boudou and Andreas Fellner and Bruno Woltzenlogel Paleo}, 
Booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 19-22, 2014. Proceedings}, 
Doi = {10.1007/978-3-319-08587-6_29}, 
Pages = {374--380}, 
Timestamp = {Mon, 13 Oct 2014 13:39:45 +0200}, 
Title = {Skeptik: A Proof Compression System}, 
  editor    = {St{\'{e}}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  series    = lncs,
  volume    = {8562},
  publisher = {Springer},
  year      = {2014},
}

@inproceedings{B38, 
Author = {Joseph Boudou and Bruno Woltzenlogel Paleo}, 
Booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, {TABLEAUX} 2013, Nancy, France, September 16-19, 2013. Proceedings}, 
Pages = {59--73}, 
Title = {Compression of Propositional Resolution Proofs by Lowering Subproofs}, 
Year = {2013},
  editor    = {Didier Galmiche and
               Dominique Larchey{-}Wendling},
  series    = {Lecture Notes in Computer Science},
  volume    = {8123},
  publisher = {Springer},
}

@inproceedings{B28, 
Author = {Pascal Fontaine and Stephan Merz and Bruno Woltzenlogel Paleo}, 
Booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings}, 
Pages = {237--251}, 
Title = {Compression of Propositional Resolution Proofs via Partial Regularization}, 
Year = {2011},
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie{-}Stokkermans},
  series    = lncs,
  volume    = {6803},
  publisher = {Springer},
}



@article{Amjad07, 
  author    = {Hasan Amjad}, 
  title     = {Compressing Propositional Refutations}, 
  journal   = {Electr. Notes Theor. Comput. Sci.}, 
  volume    = {185}, 
  year      = {2007}, 
  pages     = {3-15}, 
  ee        = {http://dx.doi.org/10.1016/j.entcs.2007.05.025}, 
  bibsource = {DBLP, http://dblp.uni-trier.de} 
} 


@incollection{CottonSplit, 
  author    = {Cotton, Scott}, 
  title     = {Two Techniques for Minimizing Resolution Proofs}, 
  year      = {2010}, 
  isbn      = {978-3-642-14185-0}, 
  booktitle = {Theory and Applications of Satisfiability Testing – SAT 2010}, 
  volume    = {6175}, 
  series    = {Lecture Notes in Computer Science}, 
  editor    = {Strichman, Ofer and Szeider, Stefan}, 
  ee        = {http://dx.doi.org/10.1007/978-3-642-14186-7_26}, 
  publisher = {Springer}, 
  pages     = {306-312} 
} 


@incollection{RedRec, 
  author    = {Rollini, Simone Fulvio and 
               Bruttomesso, Roberto and 
               Sharygina, Natasha}, 
  title     = {An Efficient and Flexible Approach to Resolution Proof Reduction}, 
  year      = {2011}, 
  isbn      = {978-3-642-19582-2}, 
  booktitle = {Hardware and Software: Verification and Testing}, 
  volume    = {6504}, 
  series    = {Lecture Notes in Computer Science}, 
  editor    = {Barner, Sharon and Harris, Ian and Kroening, Daniel and Raz, Orna}, 
  ee        = {http://dx.doi.org/10.1007/978-3-642-19583-9_17}, 
  publisher = {Springer}, 
  pages     = {182-196} 
} 

@inproceedings{RP08, 
  author    = {Omer Bar-Ilan and 
               Oded Fuhrmann and 
               Shlomo Hoory and 
               Ohad Shacham and 
               Ofer Strichman}, 
  title     = {Linear-Time Reductions of Resolution Proofs}, 
  booktitle = {Haifa Verification Conference}, 
  pages     = {114-128}, 
  editor    = {Hana Chockler and
               Alan J. Hu},
  series    = {Lecture Notes in Computer Science},
  volume    = {5394},
  publisher = {Springer},
  year      = {2009},
}
@article{RP11, 
  author    = {Omer Bar-Ilan and 
               Oded Fuhrmann and 
               Shlomo Hoory and 
               Ohad Shacham and 
               Ofer Strichman}, 
  title     = {Reducing the size of resolution proofs in linear time}, 
  journal   = {STTT}, 
  volume    = {13}, 
  number    = {3}, 
  year      = {2011}, 
  pages     = {263-272}, 
  ee        = {http://dx.doi.org/10.1007/s10009-010-0167-5}, 
  bibsource = {DBLP, http://dblp.uni-trier.de} 
} 


@inproceedings{Sinz, 
  author    = {Carsten Sinz}, 
  title     = {Compressing Propositional Proofs by Common Subproof Extraction}, 
  booktitle = {EUROCAST}, 
  year      = {2007}, 
  pages     = {547-555}, 
  ee        = {http://dx.doi.org/10.1007/978-3-540-75867-9_69}, 
  editor    = {Roberto Moreno{-}D{\'{\i}}az and
               Franz Pichler and
               Alexis Quesada{-}Arencibia},
  series    = lncs,
  volume    = {4739},
  publisher = {Springer},
}