@inproceedings(DBLP:conf/aaai/BalyoHJ17, author = {Tom{\'{a}}s Balyo and Marijn J.~H. Heule and Matti J{\"{a}}rvisalo}, year = {2017}, title = {{SAT} Competition 2016: Recent Developments}, booktitle = {Proceedings of the Thirty-First {AAAI} Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, {USA.}}, pages = {5061--5063}, ) @article(DBLP:journals/jar/BlanchetteFLW18, author = {Jasmin~Christian Blanchette and Mathias Fleury and Peter Lammich and Christoph Weidenbach}, year = {2018}, title = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and Incrementality}, journal = {J. Autom. Reasoning}, volume = {61}, number = {1-4}, pages = {333--365}, doi = {10.1007/s10817-018-9455-7}, ) @inproceedings(DBLP:conf/sat/BrummayerLB10, author = {Robert Brummayer and Florian Lonsing and Armin Biere}, year = {2010}, title = {Automated Testing and Debugging of {SAT} and {QBF} Solvers}, booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2010, 13th International Conference, {SAT} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, pages = {44--57}, doi = {10.1007/978-3-642-14186-7\_6}, ) @article(DBLP:journals/jsat/CokDW14, author = {David~R. Cok and David D{\'{e}}harbe and Tjark Weber}, year = {2014}, title = {The 2014 {SMT} Competition}, journal = {{JSAT}}, volume = {9}, pages = {207--242}, ) @inproceedings(DBLP:conf/nfm/Fleury19, author = {Mathias Fleury}, year = {2019}, title = {Optimizing a Verified {SAT} Solver}, booktitle = {{NASA} Formal Methods - 11th International Symposium, {NFM} 2019, Houston, TX, USA, May 7-9, 2019, Proceedings}, pages = {148--165}, doi = {10.1007/978-3-030-20652-9\_10}, ) @article(dafnyReferenceManual, author = {Richard~L. Ford and K.~Rustan~M. Leino}, year = {2017}, title = {Dafny Reference Manual}, ) @incollection(DBLP:reference/fai/GomesKSS08, author = {Carla~P. Gomes and Henry~A. Kautz and Ashish Sabharwal and Bart Selman}, year = {2008}, title = {Satisfiability Solvers}, booktitle = {Handbook of Knowledge Representation}, publisher = {Elsevier}, pages = {89--134}, doi = {10.1016/S1574-6526(07)03002-7}, ) @inproceedings(sel4, author = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood}, year = {2009}, title = {seL4: formal verification of an {OS} kernel}, booktitle = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles 2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009}, pages = {207--220}, doi = {10.1145/1629575.1629596}, ) @article(compcert, author = {Xavier Leroy}, year = {2009}, title = {Formal verification of a realistic compiler}, journal = {Commun. {ACM}}, volume = {52}, number = {7}, pages = {107--115}, doi = {10.1145/1538788.1538814}, ) @phdthesis(lescuyer:tel-00713668, author = {Stephane Lescuyer}, year = {2011}, title = {Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq}, type = {Theses}, school = {{Universit{\'e} Paris Sud - Paris XI}}, ) @article(DBLP:journals/jar/Maric09, author = {Filip Mari{\'{c}}}, year = {2009}, title = {Formalization and Implementation of Modern {SAT} Solvers}, journal = {J. Autom. Reasoning}, volume = {43}, number = {1}, pages = {81--119}, doi = {10.1007/s10817-009-9127-8}, ) @inproceedings(DBLP:conf/vmcai/OeSOC12, author = {Duckki Oe and Aaron Stump and Corey Oliver and Kevin Clancy}, year = {2012}, title = {versat: {A} Verified Modern {SAT} Solver}, booktitle = {Verification, Model Checking, and Abstract Interpretation - 13th International Conference, {VMCAI} 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings}, pages = {363--378}, doi = {10.1007/978-3-642-27940-9\_24}, ) @article(DBLP:journals/entcs/ShankarV11, author = {Natarajan Shankar and Marc Vaucher}, year = {2011}, title = {The Mechanical Verification of a DPLL-Based Satisfiability Solver}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {269}, pages = {3--17}, doi = {10.1016/j.entcs.2011.03.002}, ) @article(DBLP:journals/aicom/Sutcliffe18, author = {Geoff Sutcliffe}, year = {2018}, title = {The 9th {IJCAR} Automated Theorem Proving System Competition - {CASC-J9}}, journal = {{AI} Commun.}, volume = {31}, number = {6}, pages = {495--507}, doi = {10.3233/AIC-180773}, )