From 8cf7e9078de8b1e125f0a3e4f60906ba96d47ab0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg=20Schurr?= <hansjoerg-schurr@uiowa.edu> Date: Fri, 10 Feb 2023 10:47:34 -0600 Subject: [PATCH] Filter publications database to the entries we use --- spec/publications.bib | 1548 +++-------------------------------------- 1 file changed, 113 insertions(+), 1435 deletions(-) diff --git a/spec/publications.bib b/spec/publications.bib index 405318a..5921fdc 100644 --- a/spec/publications.bib +++ b/spec/publications.bib @@ -1,1437 +1,115 @@ -@misc{smtcomp21-rules, - title = "16th International Satisfiability Modulo Theories Competition ({SMT-COMP 2021}): Rules and Procedures", - author = "Barbosa, Haniel and Hoenicke, Jochen and Hyvarinen Antti", - howpublished = "\href{https://smt-comp.github.io/2021/rules.pdf}", - year = 2021, - note = "Accessed: 2021-08-08" -} - -@inproceedings{pulp, - title={{PuLP} : A Linear Programming Toolkit for {Python}}, - author={Stuart Mitchell and Michael O'Sullivan and Iain Dunning}, - year={2011} -} - -@misc{par2, - author = {Marijn Heule and Matti Järvisalo and Martin Suda}, - title = {{SAT} Race 2019}, - howpublished = {\href{http://sat-race-2019.ciirc.cvut.cz/}}, - year = 2019, - note = "Accessed: 2022-02-28" -} - -@inproceedings{gridtpt, - TITLE = {{GridTPT}: a distributed platform for Theorem Prover Testing}, - AUTHOR = {Bouton, Thomas and Caminha B. De Oliveira, Diego and D{\'e}harbe, David and Fontaine, Pascal}, - BOOKTITLE = {PAAR 2}, - ADDRESS = {Edinburgh, United Kingdom}, - YEAR = {2010}, - pages={33--39}, - MONTH = jul, -} - -@inbook{manzano-1993, - author = {Manzano, Mar\'{\i}a}, - title = {Introduction to Many-Sorted Logic}, - year = {1993}, - isbn = {0471934852}, - publisher = {John Wiley & Sons, Inc.}, - address = {USA}, - booktitle = {Many-Sorted Logic and Its Applications}, - pages = {3--86}, - month=jan, - numpages = {84} -} - -@inproceedings{wolf-1998, - author = {Wolf, Andreas and Letz, Reinhold}, - title = {Strategy Parallelism in Automated Theorem Proving}, - year = {1998}, - doi = {10.5555/646811.706867}, - publisher = {AAAI Press}, - booktitle = {Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference}, - pages = {142--146}, - numpages = {5} -} - -@article{blanchette-2013, - author = {Jasmin Christian Blanchette and - Sascha B{\"{o}}hme and - Lawrence C. Paulson}, - title = {Extending Sledgehammer with {SMT} Solvers}, - journal = {Journal of Automated Reasoning}, - volume = {51}, - number = {1}, - pages = {109--128}, - year = {2013}, - doi = {10.1007/s10817-013-9278-5}, -} - -@article{tamel-1997, - author = {Tammet, Tanel}, - title = {Gandalf}, - year = {1997}, - doi = {10.1023/A:1005887414560}, - journal = {Journal of Automated Reasoning}, - pages = {199--204}, - volume = {18}, - number = {2}, -} - - -@article{kuehlwein-2015, - author = {K\"{u}hlwein, Daniel and Urban, Josef}, - title = {{MaLeS}: A Framework for Automatic Tuning of Automated Theorem Provers}, - year = {2015}, - publisher = {Springer}, - address = {Berlin, Heidelberg}, - volume = {55}, - number = {2}, - doi = {10.1007/s10817-015-9329-1}, - journal = {Journal of Automated Reasoning}, - month = {aug}, - pages = {91-–116}, - numpages = {26}, -} - -@incollection{rice-1976, - title = {The Algorithm Selection Problem}, - editor = {Morris Rubinoff and Marshall C. Yovits}, - series = {Advances in Computers}, - publisher = {Elsevier}, - volume = {15}, - pages = {65--118}, - year = {1976}, - doi = {10.1016/S0065-2458(08)60520-3}, - author = {John R. Rice}, -} - -@article{hutter-2009, - author = {Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin and St\"{u}tzle, Thomas}, - title = {{ParamILS}: An Automatic Algorithm Configuration Framework}, - year = {2009}, - publisher = {AI Access Foundation}, - address = {El Segundo, CA, USA}, - volume = {36}, - number = {1}, - doi = {10.5555/1734953.1734959}, - journal = {Journal of Artificial Intelligence Research}, - month = {sep}, - pages = {267--306}, - numpages = {40} -} - -@inproceedings{urban-2015, - author = {Josef Urban}, - title = {{BliStr}: The Blind Strategymaker}, - booktitle = {GCAI 2015}, - editor = {Georg Gottlob and Geoff Sutcliffe and Andrei Voronkov}, - series = {EPiC Series in Computing}, - volume = {36}, - pages = {312--319}, - year = {2015}, - publisher = {EasyChair}, - issn = {2398-7340}, - doi = {10.29007/8n7m} -} - -@misc{casc-15-gandalf, - author = {Tanel Tammet}, - title = {Gandalf c-1.1}, - howpublished = {\href{http://www.tptp.org/CASC/15/SystemDescriptions.html#Gandalf}}, - year = 1998, - note = "Accessed: 2022-03-24" -} - -@article{riazanov-2003, - author = {Riazanov, Alexandre and Voronkov, Andrei}, - title = {Limited Resource Strategy in Resolution Theorem Proving}, - year = {2003}, - issue_date = {July 2003}, - publisher = {Academic Press, Inc.}, - address = {USA}, - volume = {36}, - number = {1–2}, - doi = {10.1016/S0747-7171(03)00040-3}, - journal = {Journal of Symbolic Computation}, - month = {jul}, - pages = {101--115}, - numpages = {15} -} - -@InProceedings{wenzel-2013, - author="Wenzel, Makarius", - editor="Blazy, Sandrine - and Paulin-Mohring, Christine - and Pichardie, David", - title="Shared-Memory Multiprocessing for Interactive Theorem Proving", - booktitle="ITP 4", - year="2013", - publisher="Springer Berlin Heidelberg", - pages="418--434", - doi="10.1007/978-3-642-39634-2_30" -} - -@InProceedings{desharnais-2022, - author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius}, - title = {{Seventeen Provers Under the Hammer}}, - booktitle = {ITP 13}, - pages = {8:1--8:18}, - series = {Leibniz International Proceedings in Informatics (LIPIcs)}, - year = {2022}, - volume = {237}, - editor = {Andronick, June and de Moura, Leonardo}, - publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, - address = {Dagstuhl, Germany}, - doi = {10.4230/LIPIcs.ITP.2022.8}, -} - -@misc{weber-2018, - author = {Tjark Weber}, - title = {{Par4}}, - howpublished = {\href{http://smt2019.galois.com/papers/tool_paper_9.pdf}}, - year = 2018, - note = "SMT-COMP 2018 system description. Accessed: 2022-03-30" -} - -@inproceedings{balunovic-2018, - author = {Balunovi\'{c}, Mislav and Bielik, Pavol and Vechev, Martin}, - title = {Learning to Solve {SMT} Formulas}, - year = {2018}, - publisher = {Curran Associates Inc.}, - booktitle = {NIPS 32}, - pages = {10338--10349}, - doi = {10.5555/3327546.3327694}, - numpages = {12}, - location = {Montr\'{e}al, Canada}, -} - -@inbook{demoura-2013, - author="de Moura, Leonardo - and Passmore, Grant Olney", - editor="Bonacina, Maria Paola - and Stickel, Mark E.", - title="The Strategy Challenge in {SMT} Solving", - bookTitle="Automated Reasoning and Mathematics: Essays in Memory of William W. McCune", - year="2013", - publisher="Springer", - address="Berlin, Heidelberg", - pages="15--44", - doi="10.1007/978-3-642-36675-8_2", -} - -@inproceedings{ReyEtAl-FROCOS-17, - author = {Andrew Reynolds and - Cesare Tinelli and - Dejan Jovanovic and - Clark W. Barrett}, - title = {Designing Theory Solvers with Extensions}, - booktitle = {FroCoS 11}, - pages = {22--40}, - doi = {10.1007/978-3-319-66167-4\_2}, - editor = {Clare Dixon and - Marcelo Finger}, - series = {Lecture Notes in Computer Science}, - volume = {10483}, - publisher = {Springer}, - year = {2017}, -} - -@InProceedings{scott-2021, - author="Scott, Joseph - and Niemetz, Aina - and Preiner, Mathias - and Nejati, Saeed - and Ganesh, Vijay", - editor="Groote, Jan Friso - and Larsen, Kim Guldstrand", - title="MachSMT: A Machine Learning-based Algorithm Selector for {SMT} Solvers", - booktitle="TACAS 27", - year="2021", - doi="10.1007/978-3-030-72013-1_16", - publisher="Springer International Publishing", - address="Cham", - pages="303--325" -} - -@article{burel-2020, - author = {Guillaume Burel and - Guillaume Bury and - Rapha{\"{e}}l Cauderlier and - David Delahaye and - Pierre Halmagrand and - Olivier Hermant}, - title = {First-Order Automated Reasoning with Theories: When Deduction Modulo - Theory Meets Practice}, - journal = {Journal of Automated Reasoning}, - volume = {64}, - number = {6}, - pages = {1001--1050}, - year = {2020}, - doi = {10.1007/s10817-019-09533-z}, -} - -@article{dowek-2015, - author = {Gilles Dowek}, - title = {Deduction modulo theory}, - journal = {CoRR}, - volume = {abs/1501.06523}, - year = {2015}, - url = {http://arxiv.org/abs/1501.06523}, - eprinttype = {arXiv}, - eprint = {1501.06523}, - timestamp = {Mon, 13 Aug 2018 16:47:14 +0200}, - biburl = {https://dblp.org/rec/journals/corr/Dowek15a.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@article{xu-2008, - author = {Xu, Lin and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin}, - title = {{SATzilla}: Portfolio-Based Algorithm Selection for {SAT}}, - year = {2008}, - issue_date = {May 2008}, - publisher = {AI Access Foundation}, - address = {El Segundo, CA, USA}, - volume = {32}, - number = {1}, - journal = {Journal of Artificial Intelligence Research}, - month = {jun}, - doi = {10.5555/1622673.1622687}, - pages = {565--606}, - numpages = {42} -} - -@InProceedings{barbosa-2022, - author="Barbosa, Haniel - and Barrett, Clark - and Brain, Martin - and Kremer, Gereon - and Lachnitt, Hanna - and Mann, Makai - and Mohamed, Abdalrhman - and Mohamed, Mudathir - and Niemetz, Aina - and N{\"o}tzli, Andres - and Ozdemir, Alex - and Preiner, Mathias - and Reynolds, Andrew - and Sheng, Ying - and Tinelli, Cesare - and Zohar, Yoni", - editor="Fisman, Dana - and Rosu, Grigore", - title="{cvc5}: A Versatile and Industrial-Strength {SMT} Solver", - booktitle="TACAS 28", - year="2022", - publisher="Springer International Publishing", - address="Cham", - pages="415--442", - doi="10.1007/978-3-030-99524-9_24" -} - -@InProceedings{barbosa-2017, - author = "Barbosa, Haniel - and Fontaine, Pascal - and Reynolds, Andrew", - editor = "Legay, Axel - and Margaria, Tiziana", - title = "Congruence Closure with Free Variables", - booktitle = "TACAS 23", - year = "2017", - series = {Lecture Notes in Computer Science}, - volume = "10206", - publisher = "Springer Berlin Heidelberg", - pages = "214--230", - doi = {10.1007/978-3-662-54580-5\_13} -} - -@phdthesis{barbosa-2017-phd, - author = {Haniel Barbosa}, - title = {New techniques for instantiation and proof production in {SMT} solving. - (Nouvelles techniques pour l'instanciation et la production des preuves - dans {SMT)}}, - school = {University of Lorraine, Nancy, France}, - year = {2017}, - url = {https://tel.archives-ouvertes.fr/tel-01591108}, -} - -@InProceedings{vampire, -author="Kov{\'a}cs, Laura -and Voronkov, Andrei", -editor="Sharygina, Natasha -and Veith, Helmut", -title="First-Order Theorem Proving and {Vampire}", -booktitle="CAV 25", -year="2013", -publisher="Springer Berlin Heidelberg", -pages="1--35", -isbn="978-3-642-39799-8", -doi={10.1007/978-3-642-39799-8\_1} -} - -@InProceedings{SMTCoq, - author = "Ekici, Burak - and Mebsout, Alain - and Tinelli, Cesare - and Keller, Chantal - and Katz, Guy - and Reynolds, Andrew - and Barrett, Clark", - editor = "Majumdar, Rupak - and Kun{\v{c}}ak, Viktor", - title = "{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into {C}oq", - booktitle = "CAV 29", - series = {Lecture Notes in Computer Science}, - volume = {10426}, - year = "2017", - publisher = "Springer", - pages = "126--133", - isbn = "978-3-319-63390-9", - doi = {10.1007/978-3-319-63390-9\_7} -} - -@INPROCEEDINGS{reynolds-2014, - author={Andrew {Reynolds} and Cesare {Tinelli} and Leonardo {de Moura}}, - booktitle={{FMCAD} 14}, - title={Finding conflicting instances of quantified formulas in {SMT}}, - doi = {10.1109/FMCAD.2014.6987613}, - year = {2014}, - publisher = {IEEE}, - pages = {195-202}, -} - -@inproceedings{verit, - author = {Thomas Bouton - and Diego C. B. de Oliveira - and David D{\'{e}}harbe - and Pascal Fontaine}, - title = {{veriT}: An Open, Trustable and Efficient {SMT}-solver}, - booktitle = "CADE 22", - pages = {151--156}, - year = {2009}, - editor = {Renate A. Schmidt}, - series = {Lecture Notes in Computer Science}, - volume = {5663}, - publisher = "Springer Berlin Heidelberg", - doi = {10.1007/978-3-642-02959-2_12} -} - -@inproceedings{CVC4, - author="Barrett, Clark - and Conway, Christopher L. - and Deters, Morgan - and Hadarean, Liana - and Jovanovi{\'{c}}, Dejan - and King, Tim - and Reynolds, Andrew - and Tinelli, Cesare", - editor = "Gopalakrishnan, Ganesh - and Qadeer, Shaz", - title = {{CVC4}}, - booktitle = "CAV 23", - year = "2011", - series = {Lecture Notes in Computer Science}, - volume = {6806}, - publisher = "Springer Berlin Heidelberg", - pages = "171--177", - doi = {10.1007/978-3-642-22110-1_14} -} - -@inproceedings{reynolds-2018, - author = {Andrew Reynolds and - Haniel Barbosa and - Pascal Fontaine}, - title = {Revisiting Enumerative Instantiation}, - booktitle = {TACAS 24}, - pages = {112--131}, - year = {2018}, - doi = {10.1007/978-3-319-89963-3_7}, - editor = {Dirk Beyer and - Marieke Huisman}, - series = {Lecture Notes in Computer Science}, - volume = {10806}, - publisher = {Springer International Publishing} -} - -@InProceedings{Z3, - author = "de Moura, Leonardo - and Bj{\o}rner, Nikolaj", - editor = "Ramakrishnan, C. R. - and Rehof, Jakob", - title = "{Z3}: An Efficient {SMT} Solver", - booktitle = "TACAS 14", - volume = {4963}, - series = {Lecture Notes in Computer Science}, - year = "2008", - publisher = "Springer Berlin Heidelberg", - pages = "337--340", - doi = {10.1007/978-3-540-78800-3_24} -} - -@TECHREPORT{SMTLIB, - author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli}, - title = {{The SMT-LIB Standard: Version 2.6}}, - institution = {Department of Computer Science, The University of Iowa}, - year = 2017, - note = {Available at \texttt{www.SMT-LIB.org}} -} - - -@incollection{barrett-2021, - author={Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli}, - editor = {Biere, Armin and Heule, Marijn and van Maaren, Hans and Walsh, Toby}, - title = {Satisfiability Modulo Theories}, - booktitle = {Handbook of Satisfiability}, - title = {Satisfiability Modulo Theories}, - booktitle = {Handbook of Satisfiability -- Second Edition}, - series = {Frontiers in Artificial Intelligence and Applications}, - volume = {336}, - pages = {1267--1329}, - publisher = {{IOS} Press}, - year = {2021}, - doi = {10.3233/FAIA201017}, -} - -@InProceedings{yeting-2007, - author="Ge, Yeting - and Barrett, Clark - and Tinelli, Cesare", - editor="Pfenning, Frank", - title="Solving Quantified Verification Conditions Using Satisfiability Modulo Theories", - booktitle="CADE 21", - year="2007", - publisher="Springer Berlin Heidelberg", - pages="167--182", - doi={10.1007/978-3-540-73595-3_12} -} - -@InProceedings{demoura-2007, - author="de Moura, Leonardo - and Bj{\o}rner, Nikolaj", - editor="Pfenning, Frank", - title="Efficient {E}-Matching for {SMT} Solvers", - booktitle="CADE 21", - year="2007", - publisher="Springer Berlin Heidelberg", - pages="183--198", - doi={10.1007/978-3-540-73595-3\_13} -} - -@article{detlefs-2005, - author = {Detlefs, David and Nelson, Greg and Saxe, James B.}, - title = {{Simplify}: A Theorem Prover for Program Checking}, - year = {2005}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {52}, - number = {3}, - issn = {0004-5411}, - doi = {10.1145/1066100.1066102}, - journal = {Journal of the ACM}, - month = may, - pages = {365–473}, - numpages = {109}, -} - -@article{nelson-1979, -author = {Nelson, Greg and Oppen, Derek C.}, -title = {Simplification by Cooperating Decision Procedures}, -year = {1979}, -publisher = {Association for Computing Machinery}, -address = {New York, NY, USA}, -volume = {1}, -number = {2}, -doi = {10.1145/357073.357079}, -journal = {ACM Transactions on Programming Languages and Systems}, -month = {oct}, -pages = {245--257}, -numpages = {13} -} - -@InProceedings{yeting-2009, - author="Ge, Yeting - and de Moura, Leonardo", - editor="Bouajjani, Ahmed - and Maler, Oded", - title="Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories", - booktitle="CAV 21", - year="2009", - publisher="Springer Berlin Heidelberg", - pages="306--320", - doi={10.1007/978-3-642-02658-4_25} -} - -@inbook{sekar-2001, - author = {Sekar, R. and Ramakrishnan, I. V. and Voronkov, Andrei}, - title = {Term Indexing}, - year = {2001}, - isbn = {0444508120}, - publisher = {Elsevier Science Publishers B. V.}, - address = {Amsterdam, Netherlands}, - booktitle = {Handbook of Automated Reasoning}, - pages = {1853--1964}, - numpages = {112}, - doi={10.5555/778522.778535} -} - -@inproceedings{besson-2011, - title = {A Flexible Proof Format for {SMT}: A Proposal}, - author = {Besson, Fr{\'e}d{\'e}ric and Fontaine, Pascal and Th{\'e}ry, Laurent}, - editor = "Pascal Fontaine and Aaron Stump", - booktitle = {PxTP 1}, - year = {2011}, - pages = "15--26", - url = {https://hal.inria.fr/hal-00642544/}, - month = Aug, -} - -@inproceedings{deharbe-2011, - TITLE = {Quantifier Inference Rules for {SMT} Proofs}, - AUTHOR = {D{\'e}harbe, David and Fontaine, Pascal and Woltzenlogel Paleo, Bruno}, - editor = "Pascal Fontaine and Aaron Stump", - BOOKTITLE = {PxTP 1}, - YEAR = {2011}, - pages = "33--39", - MONTH = Aug, - url = {https://hal.inria.fr/hal-00642535} -} - - -@article{martelli-1982, - author = {Martelli, Alberto and Montanari, Ugo}, - title = {An Efficient Unification Algorithm}, - year = {1982}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {4}, - number = {2}, - doi = {10.1145/357162.357169}, - journal = {ACM Transactions on Programming Languages and Systems}, - month = apr, - pages = {258-–282}, - numpages = {25} -} - -@incollection{baaz-2001, - title = {Chapter 5 -- Normal Form Transformations}, - editor = {Alan Robinson and Andrei Voronkov}, - booktitle = {Handbook of Automated Reasoning}, - publisher = {North-Holland}, - address = {Amsterdam}, - pages = {273--333}, - year = {2001}, - series = {Handbook of Automated Reasoning}, - doi = {10.1016/B978-044450813-3/50007-2}, - author = {Matthias Baaz and Uwe Egly and Alexander Leitsch and Jean Goubault-Larrecq and David Plaisted} -} - -@InProceedings{schurr-2021, -author="Schurr, Hans-J{\"o}rg -and Fleury, Mathias -and Desharnais, Martin", -editor="Platzer, Andr{\'e} -and Sutcliffe, Geoff", -title="Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant", -booktitle="CADE 28", -year="2021", -publisher="Springer International Publishing", -address="Cham", -pages="450--467", -series = {Lecture Notes in Computer Science}, -doi= {10.1007/978-3-030-79876-5_26} -} - -@inproceedings{schurr-2021a, - author = "Fontaine, Pascal - and Schurr, Hans-J{\"o}rg", - editor = "Konev, Boris and Reger, Giles", - title = "Quantifier Simplification by Unification in SMT", - booktitle = "FroCoS 13", - year = "2021", - publisher = "Springer International Publishing", - address = "Cham", - pages = "232--249", - doi = "10.1007/978-3-030-86205-3_13", -} - - -@article{robinson-1965, -author = {Robinson, John Alan}, -title = {A Machine-Oriented Logic Based on the Resolution Principle}, -year = {1965}, -publisher = {Association for Computing Machinery}, -address = {New York, NY, USA}, -volume = {12}, -number = {1}, -doi = {10.1145/321250.321253}, -journal = {Journal of the ACM}, -month = jan, -pages = {23–41}, -numpages = {19} -} - -@article{bonacina-2011, - author = {Bonacina, Maria Paola and Lynch, Christopher and de Moura, Leonardo}, - year = {2011}, - month = {08}, - pages = {161-189}, - title = {On Deciding Satisfiability by Theorem Proving with Speculative Inferences}, - volume = {47}, - journal = {Journal of Automated Reasoning}, - doi = {10.1007/s10817-010-9213-y} -} - -@InProceedings{demoura-2008, -author="de Moura, Leonardo -and Bj{\o}rner, Nikolaj", -editor="Armando, Alessandro -and Baumgartner, Peter -and Dowek, Gilles", -title="Engineering {DPLL(T)} + Saturation", -year="2008", -publisher="Springer Berlin Heidelberg", -pages="475--490", -doi={10.1007/978-3-540-71070-7\_40}, -booktitle="IJCAR 4", -} - -@InProceedings{voronkov-2014, -author="Voronkov, Andrei", -editor="Biere, Armin -and Bloem, Roderick", -title="{AVATAR}: The Architecture for First-Order Theorem Provers", -booktitle="CAV 26", -year="2014", -publisher="Springer International Publishing", -pages="696--710", -doi={10.1007/978-3-319-08867-9\_46}, -isbn="978-3-319-08867-9" -} - -@proceedings{zenodo, - title = {Quantifier Simplification by Unification in {SMT}}, - author = {Pascal Fontaine and Hans-Jörg Schurr}, - year = 2021, - publisher = {Zenodo}, - month = jul, - doi = {10.5281/zenodo.5088868}, -} - - -@misc{ip-tutorial, - title = "A Tutorial on Integer Programming", - author = "Gérard Cornuéjols and Michael A. Trick and Matthew J. Saltzman", - howpublished = "\href{https://www.math.clemson.edu/~mjs/courses/mthsc.440/integer.pdf}", - year = 1995, - note = "Accessed: 2022-04-07" -} - -@inproceedings{fontaine-21, - author = "Fontaine, Pascal - and Schurr, Hans-J{\"o}rg", - editor = "Konev, Boris and Reger, Giles", - title = "Quantifier Simplification by Unification in {SMT}", - booktitle = "Frontiers of Combining Systems", - year = "2021", - publisher = "Springer International Publishing", - address = "Cham", - pages = "232--249", - doi = "10.1007/978-3-030-86205-3_13", -} - -@misc{tange_2021_5123056, - author = {Tange, Ole}, - title = {{GNU} Parallel 20210722 ('Blue Unity')}, - month = jul, - year = 2021, - note = {{GNU Parallel is a general parallelizer to run - multiple serial command line programs in parallel - without changing them.}}, - publisher = {Zenodo}, - doi = {10.5281/zenodo.5123056}, - url = {https://doi.org/10.5281/zenodo.5123056} -} - -@article{nieuwenhuis-06, - author = {Nieuwenhuis, Robert and Oliveras, Albert and Tinelli, Cesare}, - title = {Solving {SAT} and {SAT} Modulo Theories: From an Abstract Davis--Putnam--Logemann--Loveland Procedure to DPLL(T)}, - year = {2006}, - issue_date = {November 2006}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {53}, - number = {6}, - doi = {10.1145/1217856.1217859}, - journal = {Journal of the ACM}, - month = {nov}, - pages = {937--977}, - numpages = {41}, -} - -@phdthesis{dross-2014, - author = {Claire Dross}, - title = {Generic Decision Procedures for Axiomatic First-Order Theories}, - school = {Universit{\'e} Paris-Sud}, - year = 2014, - month = apr -} - -@InProceedings{leino-2016, -author="Leino, K. R. M. -and Pit-Claudel, Cl{\'e}ment", -editor="Chaudhuri, Swarat -and Farzan, Azadeh", -title="Trigger Selection Strategies to Stabilize Program Verifiers", -booktitle="Computer Aided Verification", -year="2016", -publisher="Springer International Publishing", -address="Cham", -pages="361--381", -doi="10.1007/978-3-319-41528-4_20" -} - -@inproceedings{reynolds-2016, - author = {Andrew Reynolds}, - title = {Conflicts, Models and Heuristics for Quantifier Instantiation in {SMT}}, - booktitle = {Vampire 3}, - editor = {Laura Kovacs and Andrei Voronkov}, - series = {EPiC Series in Computing}, - volume = {44}, - pages = {1--15}, - year = {2017}, - publisher = {EasyChair}, - doi = {10.29007/jmd3} -} - -@InProceedings{blanchette-2011, - author = "Blanchette, Jasmin Christian and B{\"o}hme, Sascha and - Paulson, Lawrence C.", - editor = "Bj{\o}rner, Nikolaj and Sofronie-Stokkermans, Viorica", - title = "Extending {Sledgehammer} with {SMT} Solvers", - booktitle = "CADE 23", - year = "2011", - series = {Lecture Notes in Computer Science}, - volume = {6803}, - publisher = "Springer Berlin Heidelberg", - pages = "116--130", - doi = {10.1007/978-3-642-22438-6\_11} -} - -@InProceedings{bohme-2010, - author = "B{\"o}hme, Sascha - and Weber, Tjark", - editor = "Kaufmann, Matt - and Paulson, Lawrence C.", - title = "Fast {LCF}-Style Proof Reconstruction for {Z3}", - booktitle = "ITP 1", - series = {Lecture Notes in Computer Science}, - volume = "6172", - year = "2010", - publisher = "Springer Berlin Heidelberg", - pages = "179--194", - doi = {10.1007/978-3-642-14052-5\_14} -} - -@article{Blanchette2016-isar, - author = {Blanchette, Jasmin C. and - B{\"{o}}hme, Sascha and - Fleury, Mathias and - Smolka, Steffen J. and - Albert Steckermeier}, - title = {Semi-intelligible {I}sar Proofs from Machine-Generated Proofs}, - journal = jar, - volume = {56}, - number = {2}, - pages = {155--200}, - year = {2016}, - doi = {10.1007/s10817-015-9335-3}, -} - -@InProceedings{ebner-2021, - author="Ebner, Gabriel - and Blanchette, Jasmin - and Tourret, Sophie", - editor="Platzer, Andr{\'e} - and Sutcliffe, Geoff", - title="A Unifying Splitting Framework", - booktitle="CADE 28", - year="2021", - publisher="Springer International Publishing", - address="Cham", - doi = {10.1007/978-3-030-79876-5_20}, - pages="344--360", -} - -@inproceedings{mikolas-2021, - author="Janota, Mikoláš and Barbosa, Haniel and Fontaine, Pascal and Reynolds, Andrew", - editor="Piskac, Ruzica and Whalen, Michael W.", - title="Fair and Adventurous Enumeration of Quantifier Instantiations", - booktitle="FMCAD 21", - year=2021, - publisher="TU Wien Academic Press", - address="Vienna, Austria", - doi={10.34727/2021/isbn.978-3-85448-046-4}, - pages="256-–260" -} - -@article{barbosa-2019, - title = "Scalable Fine-Grained Proofs for Formula Processing", - journal = "Journal of Automated Reasoning", - year = {2019}, - month = jan, - author = "Barbosa, Haniel - and Blanchette, Jasmin C. - and Fleury, Mathias - and Fontaine, Pascal", - publisher = "Springer", - doi = {10.1007/s10817-018-09502-y}, -volume = {64}, - number = {3}, - pages = {485--510}, -} - -@inproceedings{fleury-2019, - author = {Mathias Fleury and - Hans{-}J{\"{o}}rg Schurr}, - editor = {Giselle Reis and - Haniel Barbosa}, - title = {Reconstructing {veriT} Proofs in {Isabelle/HOL}}, - booktitle = {PxTP 6}, - series = {{EPTCS}}, - volume = {301}, - pages = {36--50}, - year = {2019}, - doi = {10.4204/EPTCS.301.6}, -} - -@book{gordon-1979-lcf, - author = {Michael J. C. Gordon and - Robin Milner and - Christopher P. Wadsworth}, - title = {Edinburgh {LCF}: A Mechanised Logic of Computation}, - series = {Lecture Notes in Computer Science}, - volume = {78}, - publisher = {Springer Berlin Heidelberg}, - year = {1979}, - doi = {10.1007/3-540-09724-4} -} - -@inproceedings{verit-ho, - 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 International Publishing}, - year = {2019}, - doi = {10.1007/978-3-030-29436-6\_3}, -} - -@techreport{SRI:simplex:dpllt, - author = { Bruno Dutertre and Leonardo de Moura}, - title = { Integrating Simplex with {DPLL(T)} }, - year = {2006}, - month = may, - url = {http://www.csl.sri.com/users/bruno/publis/sri-csl-06-01.pdf}, - institution = { {SRI International} }, -} - -@article{schulz-2002, - author = {Stephan Schulz}, - title = {{E} -- a brainiac theorem prover}, - journal = {{AI} Communications}, - volume = {15}, - number = {2-3}, - pages = {111--126}, - year = {2002}, - publisher = {IOS Press}, -} - -@article{green-jar, - author = {Mohammad Abdulaziz and - Lawrence C. Paulson}, - title = {An {Isabelle/HOL} Formalisation of {Green}'s Theorem}, - journal = jar, - volume = {63}, - number = {3}, - pages = {763--786}, - year = {2019}, - month = nov, - doi = {10.1007/s10817-018-9495-z}, -} - -@article{Prime_Distribution_Elementary-AFP, - author = {Manuel Eberl}, - title = {Elementary Facts About the Distribution of Primes}, - journal = {Archive of Formal Proofs}, - month = feb, - url = {https://isa-afp.org/entries/Prime_Distribution_Elementary.html}, - year = 2019, - note = {Formal proof development}, - ISSN = {2150-914x}, -} - -@article{Simplex-AFP, - author = {Filip Marić and Mirko Spasić and René Thiemann}, - title = {An Incremental Simplex Algorithm with Unsatisfiable Core Generation}, - journal = {Archive of Formal Proofs}, - month = aug, - year = 2018, - url = {https://isa-afp.org/entries/Simplex.html}, - note = {Formal proof development}, - ISSN = {2150-914x}, -} - -@misc{bug-report, - author = {Fabian Immler}, - year = {2019}, - month = may, - title = {{Re: [isabelle] Isabelle2019-RC2 sporadic smt failures}}, - howpublished = {Email}, - url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-May/msg00130.html} -} - - -@article{Ordered_Resolution_Prover-AFP, - author = {Schlichtkrull, Anders and Blanchette, Jasmin C. and Traytel, Dmitriy and Waldmann, Uwe}, - title = {Formalization of {B}achmair and {G}anzinger's Ordered Resolution Prover}, - journal = {Archive of Formal Proofs}, - month = jan, - year = 2018, - url = {https://isa-afp.org/entries/Ordered_Resolution_Prover.html}, - note = {Formal proof development}, - ISSN = {2150-914x}, -} - - -@inproceedings{barbosa-2016, - author = {Haniel Barbosa}, - title = {Efficient Instantiation Techniques in {SMT} (Work In Progress)}, - pages = {1--10}, - year = {2016}, - month = jul, - url = {http://ceur-ws.org/Vol-1635/#paper-01}, - editor = {Pascal Fontaine and - Stephan Schulz and - Josef Urban}, - title = {{PAAR} 5}, - volume = {1635}, - publisher = {CEUR-WS.org}, -} - -@article{Prime_Number_Theorem-AFP, - author = {Manuel Eberl and Lawrence C. Paulson}, - title = {The Prime Number Theorem}, - journal = {Archive of Formal Proofs}, - month = sep, - year = 2018, - url = {https://isa-afp.org/entries/Prime_Number_Theorem.html}, - note = {Formal proof development}, - ISSN = {2150-914x}, -} - - -@article{Lambda_Free_KBOs-AFP, - author = {Heiko Becker and Jasmin Christian Blanchette and Uwe Waldmann and Daniel Wand}, - title = {Formalization of {Knuth–Bendix} Orders for Lambda-Free Higher-Order Terms}, - journal = {Archive of Formal Proofs}, - month = nov, - year = 2016, - url = {https://isa-afp.org/entries/Lambda_Free_KBOs.html}, - note = {Formal proof development}, - ISSN = {2150-914x}, -} - - -@article{green-afp, - author = {Mohammad Abdulaziz and Lawrence C. Paulson}, - title = {An {Isabelle/HOL} formalisation of {Green}'s Theorem}, - journal = {Archive of Formal Proofs}, - month = jan, - year = 2018, - url = {https://isa-afp.org/entries/Green.html}, - note = {Formal proof development}, - ISSN = {2150-914x}, -} -@article{meng-2009, - author = {Jia Meng and - Paulson, Lawrence C. }, - title = {Lightweight relevance filtering for machine-generated resolution problems}, - doi = {10.1016/j.jal.2007.07.004}, - journal = {Journal of Applied Logic}, - volume = {7}, - number = {1}, - pages = {41--57}, - year = {2009} +@InProceedings{ barbosa-2022, + author = "Barbosa, Haniel and Barrett, Clark and Brain, Martin and + Kremer, Gereon and Lachnitt, Hanna and Mann, Makai and + Mohamed, Abdalrhman and Mohamed, Mudathir and Niemetz, Aina + and N{\"o}tzli, Andres and Ozdemir, Alex and Preiner, + Mathias and Reynolds, Andrew and Sheng, Ying and Tinelli, + Cesare and Zohar, Yoni", + editor = "Fisman, Dana and Rosu, Grigore", + title = "{cvc5}: A Versatile and Industrial-Strength {SMT} Solver", + booktitle = "TACAS 28", + year = "2022", + publisher = "Springer International Publishing", + address = "Cham", + pages = "415--442", + doi = "10.1007/978-3-030-99524-9_24" +} + +@InProceedings{ smtcoq, + author = "Ekici, Burak and Mebsout, Alain and Tinelli, Cesare and + Keller, Chantal and Katz, Guy and Reynolds, Andrew and + Barrett, Clark", + editor = "Majumdar, Rupak and Kun{\v{c}}ak, Viktor", + title = "{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into + {C}oq", + booktitle = "CAV 29", + series = {Lecture Notes in Computer Science}, + volume = {10426}, + year = "2017", + publisher = "Springer", + pages = "126--133", + isbn = "978-3-319-63390-9", + doi = {10.1007/978-3-319-63390-9\_7} +} + +@TechReport{ smtlib, + author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli}, + title = {{The SMT-LIB Standard: Version 2.6}}, + institution = {Department of Computer Science, The University of Iowa}, + year = 2017, + note = {Available at \texttt{www.SMT-LIB.org}} +} + +@InProceedings{ besson-2011, + title = {A Flexible Proof Format for {SMT}: A Proposal}, + author = {Besson, Fr{\'e}d{\'e}ric and Fontaine, Pascal and + Th{\'e}ry, Laurent}, + editor = "Pascal Fontaine and Aaron Stump", + booktitle = {PxTP 1}, + year = {2011}, + pages = "15--26", + url = {https://hal.inria.fr/hal-00642544/}, + month = aug +} + +@InProceedings{ deharbe-2011, + title = {Quantifier Inference Rules for {SMT} Proofs}, + author = {D{\'e}harbe, David and Fontaine, Pascal and Woltzenlogel + Paleo, Bruno}, + editor = "Pascal Fontaine and Aaron Stump", + booktitle = {PxTP 1}, + year = {2011}, + pages = "33--39", + month = aug, + url = {https://hal.inria.fr/hal-00642535} +} + +@InProceedings{ schurr-2021, + author = "Schurr, Hans-J{\"o}rg and Fleury, Mathias and Desharnais, + Martin", + editor = "Platzer, Andr{\'e} and Sutcliffe, Geoff", + title = "Reliable Reconstruction of Fine-grained Proofs in a Proof + Assistant", + booktitle = "CADE 28", + year = "2021", + publisher = "Springer International Publishing", + address = "Cham", + pages = "450--467", + series = {Lecture Notes in Computer Science}, + doi = {10.1007/978-3-030-79876-5_26} +} + +@Article{ barbosa-2019, + title = "Scalable Fine-Grained Proofs for Formula Processing", + journal = "Journal of Automated Reasoning", + year = {2019}, + month = jan, + author = "Barbosa, Haniel and Blanchette, Jasmin C. and Fleury, + Mathias and Fontaine, Pascal", + publisher = "Springer", + doi = {10.1007/s10817-018-09502-y}, + volume = {64}, + number = {3}, + pages = {485--510} +} + +@InProceedings{ fleury-2019, + author = {Mathias Fleury and Hans{-}J{\"{o}}rg Schurr}, + editor = {Giselle Reis and Haniel Barbosa}, + title = {Reconstructing {veriT} Proofs in {Isabelle/HOL}}, + booktitle = {PxTP 6}, + series = {{EPTCS}}, + volume = {301}, + pages = {36--50}, + year = {2019}, + doi = {10.4204/EPTCS.301.6} +} + +@Misc{ wp:alethe, + author = "{Wikipedia contributors}", + title = "Alethe (bird) -- {Wikipedia}{,} The Free Encyclopedia", + year = "2022", + url = "https://en.wikipedia.org/w/index.php?title=Alethe_(bird)&oldid=1064503766", + note = "Online; accessed 2022-09-02" } - -@inproceedings{kuehlwein-2013, - author = {K{\"{u}}hlwein, Daniel and - Blanchette, Jasmin Christian and - Kaliszyk, Cezary and - Urban, Josef}, - 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}}, - howpublished = {Inria Internship Report}, - month = aug, - year = {2016}, - url = {http://prosecco.gforge.inria.fr/personal/hritcu/students/alejandro/report.pdf}, -} - -@misc{matryoshka, - author = {Jasmin Blanchette}, - title = {Matryoshka}, - howpublished = {Project Webpage}, - note = "Accessed: 2022-07-14", - month = july, - year = {2022}, - url = {https://matryoshka-project.github.io/#}, -} - -@inproceedings{defourne-2021, - TITLE = {Improving Automation for Higher-Order Proof Steps}, - AUTHOR = {Defourn{\'e}, Rosalie}, - BOOKTITLE = {FroCos 13}, - ADDRESS = {Birmingham, United Kingdom}, - EDITOR = {Boris Konev and Giles Reger}, - PUBLISHER = {{Springer}}, - SERIES = {FroCoS 13}, - VOLUME = {12941}, - PAGES = {139--153}, - YEAR = {2021}, - MONTH = Sep, - DOI = {10.1007/978-3-030-86205-3_8}, -} - -@misc{wp:alethe, -author = "{Wikipedia contributors}", -title = "Alethe (bird) -- {Wikipedia}{,} The Free Encyclopedia", -year = "2022", -url = "https://en.wikipedia.org/w/index.php?title=Alethe_(bird)&oldid=1064503766", -note = "Online; accessed 2022-09-02" -} - -@inproceedings{claessen-2003, -author = {Claessen, Koen and Sorensson, Niklas}, -year = {2003}, -month = {08}, -pages = {}, -title = {New Techniques that Improve {MACE}-style Finite Model Finding}, - BOOKTITLE = {MODEL}, -} - -- GitLab