In order to have more confidence in software-based systems, we would like to be able to show automatically that a particular software component meets its specification; the component does what it is supposed to do. Testing can increase confidence in software; however, testing alone cannot show that software meets its specification, only that no errors have been found yet. We are building stronger tools for increasing our confidence in software in response to the verifying compiler grand challenge. The vision is that all software will include specifications for all of the operations of a component (including pre- and post-conditions) along with code annotations in a purported implementation (including loop invariants, and progress metrics for the termination of both loops and recursive operations). These annotations allow us to generate verification conditions (VCs) that represent the correctness of the code mathematically. The code meets its specification and is correct if the VCs are proved.
We focus on the problem of automating VC proofs and examining potential obstacles for automated proofs. More specifically, this dissertation defends the following three-part thesis:
1. Modest changes in programming languages may effectively support and facilitate automated verification without introducing an undue annotation burden on programmers.
2. An interactive proof assistant can be an effective back-end prover for automated software verification.
3. Translations between similar formal systems present significant challenges in fully automating software verification.