Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich. A verified SAT solver with watched literals using imperative HOL. In June Andronick, Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. pages 158-171, ACM, 2018. [doi]
Abstract is missing.