The Mechanical Verification of a DPLL-Based Satisfiability Solver. - Natarajan Shankar; Marc Vaucher (LSFA, 2010)