Title: Development of a Verified, Efficient Checker for SAT Proofs
Speaker: Matt Kaufmann (in collaboration with Marijn Heule and Warren Hunt, Jr.)

Abstract:

I'll present a case study, consisting of a sequence of verified
checkers that validate SAT proofs.  These culminate in an efficient
checker that can be used in SAT competitions and in industry.  No
background in SAT is assumed.