Software is remarkably important to modern life. The correct and secure behavior of software that controls nearly all major machines and communications systems, from aircraft and cars to medical records and financial transactions, is mission-critical and often can be a matter of life and death. The current industry-standard method for assessing correctness of software, known as "software testing", is not foolproof. This research project will combine the interdisciplinary expertise of the investigators in software engineering and mathematical logic to support a paradigm shift toward "verified software": programs that have been entirely and mechanically proved, using formal mathematical logic, to be correct relative to full behavioral specifications of what they are supposed to do and what they are not supposed to do. Given the broad benefits of correct software to society and its impact on national competitiveness, a strong U.S. presence in verified software research and education must be a national priority.
While transition of research ideas to practice will take time, the idea of a verifying compiler for sequential, object-based software is tantalizingly close to reality. In what can be properly described as the "end game", extensive empirical studies of Verification Conditions (VCs) for correct software already have been undertaken. VCs are assertions that establish that a program is correct if and only if they can be proved. It has been observed that when VCs are not provable mechanically, the obstacles lie in proving VCs that are "obvious" to mathematicians, and in engineering specifications and supporting mathematics so they lead to VCs that are also "obvious" to automated provers. The expected results of this project are programming language- and tool-independent improvements in automated software verification that will be widely applicable. Another key project goal is integration of new concepts and tools supporting verified software into undergraduate and graduate Computer Science courses. These efforts will contribute to development of a superior next-generation software engineering workforce.
