Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 03d2f436 authored by BESSON Frederic's avatar BESSON Frederic
Browse files

paper v0

parent 15bc1eb9
No related branches found
No related tags found
No related merge requests found
@inproceedings{FleuryBL18,
author = {Mathias Fleury and
Jasmin Christian Blanchette and
Peter Lammich},
title = {A verified {SAT} solver with watched literals using imperative {HOL}},
booktitle = {CPP},
pages = {158--171},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167080},
doi = {10.1145/3167080},
timestamp = {Sat, 19 Oct 2019 20:16:55 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FleuryBL18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}}
@article{BlanchetteFLW18,
author = {Jasmin Christian Blanchette and
Mathias Fleury and
Peter Lammich and
Christoph Weidenbach},
title = { A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
Incrementality},
journal = {J. Autom. Reason.},
volume = {61},
number = {1-4},
pages = {333--365},
year = {2018},
url = {https://doi.org/10.1007/s10817-018-9455-7},
doi = {10.1007/s10817-018-9455-7},
timestamp = {Wed, 02 Sep 2020 13:30:06 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteFLW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{lescuyer08tphol,
author = {St\'ephane Lescuyer and Sylvain Conchon},
title = {{A Reflexive Formalization of a SAT Solver in Coq}},
booktitle = {Emerging Trends of TPHOLs},
year = 2008,
}
@Inbook{Tseitin1983,
author="Tseitin, G. S.",
editor="Siekmann, J{\"o}rg H.
and Wrightson, Graham",
title="On the Complexity of Derivation in Propositional Calculus",
bookTitle="Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970",
year="1983",
publisher="Springer",
address="Berlin, Heidelberg",
pages="466--483",
abstract="The question of the minimum complexity of derivation of a given formula in classical propositional calculus is considered in this article and it is proved that estimates of complexity may vary considerably among the various forms of propositional calculus. The forms of propositional calculus used in the present article are somewhat unusual, {\textdagger} but the results obtained for them can, in principle, be extended to the usual forms of propositional calculus.",
isbn="978-3-642-81955-1",
doi="10.1007/978-3-642-81955-1_28",
url="https://doi.org/10.1007/978-3-642-81955-1_28"
}
@inproceedings{SozeauO08,
author = {Matthieu Sozeau and
Nicolas Oury},
title = {First-Class Type Classes},
booktitle = {TPHOLs},
series = {LNCS},
volume = {5170},
pages = {278--293},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-71067-7\_23},
doi = {10.1007/978-3-540-71067-7\_23},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/SozeauO08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{casteran:hal-00344237,
TITLE = {{Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions.}},
AUTHOR = {Cast{\'e}ran, Pierre and Bertot, Yves},
URL = {https://hal.archives-ouvertes.fr/hal-00344237},
PUBLISHER = {{Springer Verlag}},
SERIES = {Texts in Theoretical Computer Science},
PAGES = {470},
YEAR = {2004},
HAL_ID = {hal-00344237},
HAL_VERSION = {v1},
}
@INPROCEEDINGS{Okasaki98fastmergeable,
author = {Chris Okasaki and Andrew Gill},
title = {Fast Mergeable Integer Maps},
booktitle = {In Workshop on ML},
year = {1998},
pages = {77--86}
}
@INPROCEEDINGS{Zhang96anefficient,
author = {Hantao Zhang and Mark E. Stickel},
title = {An Efficient Algorithm for Unit Propagation},
booktitle = {AI-MATH},
year = {1996},
pages = {166--169}
}
@article{ZhangS00,
author = {Hantao Zhang and
Mark E. Stickel},
title = {Implementing the Davis-Putnam Method},
journal = {J. Autom. Reason.},
volume = {24},
number = {1/2},
pages = {277--296},
year = {2000},
url = {https://doi.org/10.1023/A:1006351428454},
doi = {10.1023/A:1006351428454},
timestamp = {Wed, 02 Sep 2020 13:30:01 +0200},
biburl = {https://dblp.org/rec/journals/jar/ZhangS00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{PlaistedG86,
author = {David A. Plaisted and
Steven Greenbaum},
title = {A Structure-Preserving Clause Form Translation},
journal = {J. Symb. Comput.},
volume = {2},
number = {3},
pages = {293--304},
year = {1986},
url = {https://doi.org/10.1016/S0747-7171(86)80028-1},
doi = {10.1016/S0747-7171(86)80028-1},
timestamp = {Wed, 14 Nov 2018 10:27:10 +0100},
biburl = {https://dblp.org/rec/journals/jsc/PlaistedG86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{ClaessenR15,
author = {Koen Claessen and
Dan Ros{\'{e}}n},
title = {{SAT} Modulo Intuitionistic Implications},
booktitle = {{LPAR-20}},
series = {LNCS},
volume = {9450},
pages = {622--637},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-662-48899-7\_43},
doi = {10.1007/978-3-662-48899-7\_43},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/ClaessenR15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{LescuyerC09,
author = {St{\'{e}}phane Lescuyer and
Sylvain Conchon},
title = {Improving Coq Propositional Reasoning Using a Lazy {CNF} Conversion
Scheme},
booktitle = {FroCoS},
series = {LNCS},
volume = {5749},
pages = {287--303},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04222-5\_18},
doi = {10.1007/978-3-642-04222-5\_18},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/frocos/LescuyerC09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{Allen-hcons,
author = {Allen, John},
title = {Anatomy of LISP},
year = {1978},
isbn = {007001115X},
publisher = {McGraw-Hill, Inc.},
address = {USA},
}
@inproceedings{GanzingerHNOT04,
author = {Harald Ganzinger and
George Hagen and
Robert Nieuwenhuis and
Albert Oliveras and
Cesare Tinelli},
editor = {Rajeev Alur and
Doron A. Peled},
title = {{DPLL(} {T):} Fast Decision Procedures},
booktitle = {{CAV}},
series = {LNCS},
volume = {3114},
pages = {175--188},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-27813-9\_14},
doi = {10.1007/978-3-540-27813-9\_14},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/GanzingerHNOT04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{KornK97,
author = {Daniel S. Korn and
Christoph Kreitz},
editor = {William McCune},
title = {Deciding Intuitionistic Propositional Logic via Translation into Classical
Logic},
booktitle = {CADE},
series = {LNCS},
volume = {1249},
pages = {131--145},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-63104-6\_15},
doi = {10.1007/3-540-63104-6\_15},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/KornK97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{Corbineau06,
author = {Pierre Corbineau},
editor = {Thorsten Altenkirch and
Conor McBride},
title = {Deciding Equality in the Constructor Theory},
booktitle = {{TYPES}},
series = {LNCS},
volume = {4502},
pages = {78--92},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/978-3-540-74464-1\_6},
doi = {10.1007/978-3-540-74464-1\_6},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/Corbineau06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{Dyckhoff92,
author = {Roy Dyckhoff},
title = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
journal = {J. Symb. Log.},
volume = {57},
number = {3},
pages = {795--807},
year = {1992},
url = {https://doi.org/10.2307/2275431},
doi = {10.2307/2275431},
timestamp = {Sun, 28 May 2017 13:21:54 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Dyckhoff92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{PaulsonS07,
author = {Lawrence C. Paulson and
Kong Woei Susanto},
title = {Source-Level Proof Reconstruction for Interactive Theorem Proving},
booktitle = {TPHOLs},
series = {LNCS},
volume = {4732},
pages = {232--245},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-74591-4\_18},
doi = {10.1007/978-3-540-74591-4\_18},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/PaulsonS07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@INPROCEEDINGS{Hurd03first-orderproof,
author = {Joe Hurd},
title = {First-order proof tactics in higher-order logic theorem provers},
booktitle = {Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports},
year = {2003},
pages = {56--68}
}
@article{BlanchetteBP13,
author = {Jasmin Christian Blanchette and
Sascha B{\"{o}}hme and
Lawrence C. Paulson},
title = {Extending Sledgehammer with {SMT} Solvers},
journal = {J. Autom. Reason.},
volume = {51},
number = {1},
pages = {109--128},
year = {2013},
url = {https://doi.org/10.1007/s10817-013-9278-5},
doi = {10.1007/s10817-013-9278-5},
timestamp = {Wed, 02 Sep 2020 13:29:47 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteBP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{BessonCP11,
author = {Fr{\'{e}}d{\'{e}}ric Besson and
Pierre{-}Emmanuel Cornilleau and
David Pichardie},
title = {Modular {SMT} Proofs for Fast Reflexive Checking Inside Coq},
booktitle = {{CPP}},
series = {LNCS},
volume = {7086},
pages = {151--166},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_13},
doi = {10.1007/978-3-642-25379-9\_13},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BessonCP11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{ArmandFGKTW11,
author = {Micha{\"{e}}l Armand and
Germain Faure and
Benjamin Gr{\'{e}}goire and
Chantal Keller and
Laurent Th{\'{e}}ry and
Benjamin Werner},
title = {A Modular Integration of {SAT/SMT} Solvers to Coq through Proof Witnesses},
booktitle = {{CPP}},
series = {LNCS},
volume = {7086},
pages = {135--150},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_12},
doi = {10.1007/978-3-642-25379-9\_12},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ArmandFGKTW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{BohmeW10,
author = {Sascha B{\"{o}}hme and
Tjark Weber},
title = {Fast LCF-Style Proof Reconstruction for {Z3}},
booktitle = {{ITP}},
series = {LNCS},
volume = {6172},
pages = {179--194},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_14},
doi = {10.1007/978-3-642-14052-5\_14},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/BohmeW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DetersR0BT14,
author = {Morgan Deters and
Andrew Reynolds and
Tim King and
Clark W. Barrett and
Cesare Tinelli},
title = {A tour of {CVC4:} How it works, and how to use it},
booktitle = {{FMCAD}},
pages = {7},
publisher = {{IEEE}},
year = {2014},
url = {https://doi.org/10.1109/FMCAD.2014.6987586},
doi = {10.1109/FMCAD.2014.6987586},
timestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/DetersR0BT14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{MouraB08,
author = {Leonardo Mendon{\c{c}}a de Moura and
Nikolaj Bj{\o}rner},
title = {{Z3:} An Efficient {SMT} Solver},
booktitle = {{TACAS}},
series = {LNCS},
volume = 4963,
pages = {337--340},
publisher = {Springer},
year = 2008,
url = {https://doi.org/10.1007/978-3-540-78800-3\_24},
doi = {10.1007/978-3-540-78800-3\_24},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{BoutonODF09,
author = {Thomas Bouton and
Diego Caminha Barbosa De Oliveira and
David D{\'{e}}harbe and
Pascal Fontaine},
title = {veriT: An Open, Trustable and Efficient SMT-Solver},
booktitle = {CADE},
series = {LNCS},
volume = {5663},
pages = {151--156},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02959-2\_12},
doi = {10.1007/978-3-642-02959-2\_12},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/BoutonODF09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{ArmandGST10,
author = {Micha{\"{e}}l Armand and
Benjamin Gr{\'{e}}goire and
Arnaud Spiwack and
Laurent Th{\'{e}}ry},
title = {Extending Coq with Imperative Features and Its Application to {SAT}
Verification},
booktitle = {{ITP}},
series = {LNCS},
volume = {6172},
pages = {83--98},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_8},
doi = {10.1007/978-3-642-14052-5\_8},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/ArmandGST10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{MoskewiczMZZM01,
author = {Matthew W. Moskewicz and
Conor F. Madigan and
Ying Zhao and
Lintao Zhang and
Sharad Malik},
title = {Chaff: Engineering an Efficient {SAT} Solver},
booktitle = {{DAC}},
pages = {530--535},
publisher = {{ACM}},
year = {2001},
url = {https://doi.org/10.1145/378239.379017},
doi = {10.1145/378239.379017},
timestamp = {Wed, 14 Nov 2018 10:58:37 +0100},
biburl = {https://dblp.org/rec/conf/dac/MoskewiczMZZM01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{WeberA09,
author = {Tjark Weber and
Hasan Amjad},
title = {Efficiently checking propositional refutations in {HOL} theorem provers},
journal = {J. Appl. Log.},
volume = {7},
number = {1},
pages = {26--40},
year = {2009},
url = {https://doi.org/10.1016/j.jal.2007.07.003},
doi = {10.1016/j.jal.2007.07.003},
timestamp = {Fri, 21 Feb 2020 13:13:05 +0100},
biburl = {https://dblp.org/rec/journals/japll/WeberA09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{HarrisonT98,
author = {John Harrison and
Laurent Th{\'{e}}ry},
title = {A Skeptic's Approach to Combining {HOL} and Maple},
journal = {J. Autom. Reason.},
volume = {21},
number = {3},
pages = {279--294},
year = {1998},
url = {https://doi.org/10.1023/A:1006023127567},
doi = {10.1023/A:1006023127567},
timestamp = {Wed, 02 Sep 2020 13:29:47 +0200},
biburl = {https://dblp.org/rec/journals/jar/HarrisonT98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
/home/fbesson/sources/itauto/benchmark
\ No newline at end of file
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment