Automating interactive theorem provers and certifying automated theorem provers

Computers are ubiquitous in today's world and have been integrated into every aspect of our lives and work. They have wide-ranging applications such as in defense systems, healthcare systems, banking, and infrastructure. A computer is operated using interfaces called software. It is important to ensure that a software behaves as it is instructed to. When a software produces undesirable behavior, we call the source of this behavior a bug. Avoiding software bugs is especially important in safety-critical systems — computer systems whose misbehavior could result in serious injury or loss of life. Examples of these include software that runs airplane systems, drones, cars, medical devices, and power plants.

Given (i) a specification of how a software should behave, as a set of logical formulas, and (ii) either a model or an implementation of the software, a theorem prover is a tool that can be used to ensure that the software behaves as it's supposed to. Theorem provers can be broadly classified as automated or interactive. Automated theorem provers (ATPs) aim to prove logical formulas quickly without external human help. Achieving this takes a substantial amount of code, which makes ATPs typically large computer software that are themselves prone to bugs. On the other hand, interactive theorem provers (ITPs) are smaller pieces of software that strictly follow certain principles that prevent bugs in their code. However, they provide a limited amount of automation, and hence, proving logical formulas in an ITP requires significantly more effort from a user. An ideal tool for software verification would offer both proof automation and strict guarantees of software correctness. This thesis presents three integrations between ATPs and ITPs that leverage the higher level of automation in ATPs and the higher level of trust in the proofs produced by ITPs to offer faster and more reliable provers for software systems. Provers integrated in these ways would prevent bugs in our software.

1. External ATPs can be used within ITPs to automate proofs. Such an integration can preserve the high level of trust in the ITP by internally following the steps taken by the ATP to prove the formula. Often, an external ATP can fail in such an integration because the ATP does not have sufficient information from the ITP to prove a formula. The first contribution of this thesis enhances a typical ATP-ITP integration so that the ATP can ask for extra information to prove a currently failing goal. Our work's experimental evaluation suggests that such an enhancement reduces the number of failures that can occur when an ITP calls an external ATP to automatically prove formulas for it.

2. An ATP's result can be externally verified by checking it in an ITP. This increases trust in the results produced by an ATP. ATPs that produce additional certificates can have their results verified in an ITP. The second contribution of this thesis generates an ITP checker for certificates produced by two distinct ATPs. Our experimental evaluation argues that this checker is more complete in its coverage than previous ITP checkers for ATPs.

3. An ATP can be verified within an ITP. Although the size of modern ATPs makes this a very challenging goal, ATPs can be separated into independent modules. The final contribution of this thesis is to verify a set of results, called invertibility conditions in an ITP. For ATPs that use them, the correct operation of one of their modules depends on the correctness of these invertibility conditions. The verification of these conditions in an ITP increases the reliability of the corresponding module of the ATP that relies on them.