CPA-SEL: Collaborative Research - Continuing Progress Toward Verified Software

Ohio State University Research Foundation -Do Not Use, Columbus OH

Investigators

Abstract

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.