title={{MaSh}: Machine Learning for {Sledgehammer}},
booktitle={{ITP} 4},
series={{LNCS}},
volume={7998},
pages={35--50},
publisher={Springer},
year={2013},
doi={10.1007/978-3-642-39634-2_6}
}
@InProceedings{judgementday,
author="B{\"o}hme, Sascha and Nipkow, Tobias",
editor="Giesl, J{\"u}rgen and H{\"a}hnle, Reiner",
title="{Sledgehammer}: Judgement Day",
booktitle="IJCAR 5",
year="2010",
publisher="Springer Berlin Heidelberg",
pages="107--121",
doi={10.1007/978-3-642-14203-1_9}
}
@proceedings{schurr_hans_jorg_2021_4727349,
title={{Reliable Reconstruction of Fine-Grained Proofs in
a Proof Assistant}},
author={Hans-Jörg Schurr
and Mathias Fleury
and Martin Desharnais},
year=2021,
publisher={Zenodo},
month=apr,
doi={10.5281/zenodo.4727349},
}
@inproceedings{rodin,
TITLE={{SMT} solvers for {R}odin},
AUTHOR={D{\'e}harbe, David
and Fontaine, Pascal
and Guyot, Yoann
and Voisin, Laurent},
BOOKTITLE={{ABZ 2012}},
EDITOR={John Derrick
and John A. Fitzgerald
and Stefania Gnesi
and Sarfraz Khurshid
and Michael Leuschel
and Steve Reeves
and Elvinia Riccobene},
publisher="Springer Berlin Heidelberg",
SERIES=lncs,
VOLUME={7316},
PAGES={194-207},
YEAR={2012},
MONTH=Jun,
doi={10.1007/978-3-642-30885-7_14}
}
@inproceedings{interpolants,
author={Kenneth L. McMillan},
title={Interpolants from {Z3} proofs},
booktitle={{FMCAD} 11},
isbn={9780983567813},
publisher={FMCAD Inc},
address={Austin, Texas},
pages={19--27},
year={2011},
}
@article{mclaughlin-2006,
author={Sean McLaughlin and
Clark Barrett and
Yeting Ge},
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},
year={2006},
doi={10.1016/j.entcs.2005.12.005}
}
@inproceedings{armand-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},
title={A Modular Integration of {SAT}\slash{SMT} Solvers to {Coq} through
Proof Witnesses},
booktitle={CPP~1},
pages={135--150},
editor={Jean-Pierre Jouannaud and
Zhong Shao},
publisher={Springer Berlin Heidelberg},
series=lncs,
volume={7086},
year={2011},
doi={10.1007/978-3-642-25379-9_12}
}
@inproceedings{ekici-2017,
author={Burak Ekici and
Alain Mebsout and
Cesare Tinelli and
Chantal Keller and
Guy Katz and
Andrew Reynolds and
Clark W. Barrett},
title={{SMTCoq}: {A} Plug-In for Integrating {SMT} Solvers into {Coq}},
booktitle={CAV 29},
pages={126--133},
year={2017},
doi={10.1007/978-3-319-63390-9_7},
editor={Rupak Majumdar and
Viktor Kuncak},
series=lncs,
volume={10427},
publisher={Springer International Publishing},
}
@phdthesis{bohme-thesis,
author={Sascha B\"ohme},
title={Proving Theorems of Higher-Order Logic with {SMT} Solvers},
school={Technische Universit\"at M\"unchen},
year=2012,
url={http://mediatum.ub.tum.de/node?id=1084525}
}
@article{stump-2013,
author={Stump, Aaron and Oe, Duckki and Reynolds, Andrew and Hadarean,
Liana and Tinelli, Cesare},
title={{SMT} Proof Checking Using a Logical Framework},
journal={Formal Methods in System Design},
volume={42},
number={1},
month=feb,
year={2013},
issn={0925-9856},
pages={91--118},
numpages={28},
publisher={Kluwer Academic Publishers},
doi={10.1007/s10703-012-0163-3}
}
@inproceedings{christ-2012,
author={J{\"{u}}rgen Christ and
Jochen Hoenicke and
Alexander Nutz},
editor={Alastair F. Donaldson and
David Parker},
title={SMTInterpol: An Interpolating {SMT} Solver},
booktitle={SPIN 19},
series={Lecture Notes in Computer Science},
volume={7385},
pages={248--254},
publisher={Springer},
year={2012},
doi={10.1007/978-3-642-31759-0_19},
}
@InProceedings{hyvarinen-2016,
author="Hyv{\"a}rinen, Antti E. J.
and Marescotti, Matteo
and Alt, Leonardo
and Sharygina, Natasha",
editor="Creignou, Nadia
and Le Berre, Daniel",
title="{OpenSMT2}: An {SMT} Solver for Multi-core and Cloud Computing",
booktitle="SAT 19",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="547--553",
isbn="978-3-319-40970-2"
}
@InProceedings{barbosa-2022a,
author="Barbosa, Haniel
and Reynolds, Andrew
and Kremer, Gereon
and Lachnitt, Hanna
and Niemetz, Aina
and N{\"o}tzli, Andres
and Ozdemir, Alex
and Preiner, Mathias
and Viswanathan, Arjun
and Viteri, Scott
and Zohar, Yoni
and Tinelli, Cesare
and Barrett, Clark",
editor="Blanchette, Jasmin
and Kov{\'a}cs, Laura
and Pattinson, Dirk",
title="Flexible Proof Production in an Industrial-Strength SMT Solver",
booktitle="IJCAR 11",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="15--35",
doi={10.1007/978-3-031-10769-6_3}
}
@inproceedings{hoenicke-2022,
author={Jochen Hoenicke and
Tanja Schindler},
editor={David D{\'{e}}harbe and
Antti E. J. Hyv{\"{a}}rinen},
title={A Simple Proof Format for {SMT}},
booktitle={SMT 20},
series={{CEUR} Workshop Proceedings},
volume={3185},
pages={54--70},
publisher={CEUR-WS.org},
year={2022},
}
@inproceedings{schurr-2022,
author={Hans-Jörg Schurr},
editor={Boris Konev and
Claudia Schon and
Alexander Steen},
title={Optimal Strategy Schedules for Everyone},
booktitle={PAAR 8},
series={{CEUR} Workshop Proceedings},
volume={3201},
publisher={CEUR-WS.org},
year={2022},
}
@inproceedings{otoni-2021,
title={Theory-Specific Proof Steps Witnessing Correctness of {SMT} Executions},
booktitle={DAC 58},
year={2021},
month={11},
publisher={IEEE},
organization={IEEE},
address={San Francisco, CA, USA},
doi={10.1109/DAC18074.2021.9586272},
author={Rodrigo Otoni and Martin Blicha and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
@inproceedings{assaf-2016,
TITLE={Expressing theories in the λΠ-calculus modulo theory and in the {Dedukti} system},
AUTHOR={Assaf, Ali and Burel, Guillaume and Cauderlier, Raphal and Delahaye, David and Dowek, Gilles and Dubois, Catherine and Gilbert, Fr{\'e}d{\'e}ric and Halmagrand, Pierre and Hermant, Olivier and Saillard, Ronan},
BOOKTITLE={{TYPES}: Types for Proofs and Programs},
ADDRESS={Novi SAd, Serbia},
YEAR={2016},
MONTH=May,
}
@article{Downey1980,
author={Downey, Peter J. and Sethi, Ravi and Tarjan, Robert Endre},
title={Variations on the Common Subexpression Problem},
journal={Journal of the ACM},
volume={27},
number={4},
month=oct,
year={1980},
issn={0004-5411},
pages={758--771},
numpages={14},
doi={10.1145/322217.322228},
acmid={322228},
publisher={ACM},
address={New York, NY, USA}
}
@article{Nelson1980,
author={Nelson, Greg and Oppen, Derek C.},
title={Fast Decision Procedures Based on Congruence Closure},
journal={Journal of the ACM},
month=apr,
volume={27},
number={2},
year={1980},
pages={356--364},
numpages={9},
doi={10.1145/322186.322198},
publisher={ACM}
}
@inproceedings{biere-2020,
title={CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the {SAT} Competition 2020},
author={Armin Biere and Katalin Fazekas and Mathias Fleury and Maximilian Heisinger},
year={2020}
}
@inproceedings{barbosa-2019a,
author={Haniel Barbosa and
Andrew Reynolds and
Daniel El Ouraoui and
Cesare Tinelli and
Clark W. Barrett},
editor={Pascal Fontaine},
title={Extending {SMT} Solvers to Higher-Order Logic},
booktitle={{CADE 27}},
series={Lecture Notes in Computer Science},
volume={11716},
pages={35--54},
publisher={Springer},
year={2019},
doi={10.1007/978-3-030-29436-6\_3},
}
@misc{aguirre-2016,
author={Alejandro Aguirre},
title={Towards a Provably Correct Encoding from {F*} to {SMT}},