Most engineered artifacts, such as bridges and nuclear power plants, are tested by subjecting them to operating conditions and observing results. Software is different. It manifests dynamic behavior when running on computers, and software quality (with respect to achieving specified behavior) is normally tested that way. But software also can be considered purely symbolic -- a sequence of instructions -- and hence can be subjected to mathematical proof of correctness. Achieving such "verified software" has been identified as a "grand challenge" for computing research. The work of this project's interdisciplinary team of software engineers and logicians focuses on the thesis that practical, scalable, automated software verification is feasible, one component at a time, by combining careful language design with recent advances in automated theorem proving. The plan is to evaluate this thesis empirically by generating the logical verification conditions for a benchmark suite of software components like those used in computing courses and commercial software, and proving them automatically. The project's significance will derive from its proof of concept that the verified software grand challenge can be conquered, and from a better understanding of what the next generation of software engineers need to be taught to produce verified software.
Ultimately, the society needs to ensure that deployed software functions according to its specification. Though this project does not directly impact the problem of getting specifications themselves to match human intent, to the extent the specifications capture the intent, it addresses the problem of getting code to function in accordance. The project is interdisciplinary and it involves mathematical logic and computer science. The intellectual merit of the project is that it has led to the development of a prototype push-button verifying compiler--a compiler that checks that code meets specifications under all specified input conditions and then generates executable code. The project has fundamentally established that it is possible to develop a mechanical and modular verifying compiler--not just for simple code--but for non-tivial software involving generic, object-based components that themselves may be built using other such components, such as those we can write in modern programming languages. The modularity of the verifying compiler makes it possible to specify and verify one component at a time, making it scalable for component-based systems. A key technical result is that the project has established that no "deep thinking" is necessary to prove verification conditions (VCs) of correctness that arise, if software is suitaby designed and annotated. The implication of this result is that there is a dichotomy between the powerful provers necessary to establish non-trivial mathematical results and the provers that are suited for discharging software correctness, given those results. The project results have been validated through the development and verification of a benchmark suite of software components. The project has a had a broad impact on human and information resources, and computer science education. Eight graduate students (four of whom are women) and eight undergraduate students (four of whom are also women) have benefitted from the project. Verification techniques to produce high quality software have been integrated into graduate courses and two required undergraduate courses for CS majors at Clemson, affecting numerous students every year. For widespread research experimentation and student learning at multiple institutions, the verifying compiler has been integrated into a web-integrated environment that is freely available.
