Automating interactive theorem provers and certifying automated theorem provers

As software grows increasingly pervasive in our everyday lives, it is important to ensure that the software we rely on, especially in safety-critical systems, behaves as expected. Whereas software testing is a useful approach for detecting the presence of bugs, formal methods offer tools and techniques to prove the absence of bugs. One class of such tools is theorem provers — computer programs capable of proving mathematical theorems. Among other things, theorem provers are used to prove the correctness of software with respect to a specification, in an attempt to prevent buggy software.