The Verified Software Initiative

Presented as part of the 2007 HCSS conference.

Abstract

Software is at the core of our infrastructure. We rely on it to execute complex, sensitive, and critical functions, without any strong scientific basis for trusting its correctness. Software verification is a discipline of computing that demonstrates the correctness of programs with respect to a precise specification based on formal proofs built on a rigorous semantic foundation. Both the theory and practice of verification have witnessed accelerated progress in recent years, but we are still a long way from offering cast-iron guarantees for critical parts of our software infrastructure.

The Verified Software Initiative (VSI) is a comprehensive, long-term research program directed at the challenge of verifying software to the highest levels of correctness. This initiative, originally proposed by Professor Tony Hoare, is the culmination of several years of consensus-building within the verification research community spanning Asia, Europe, and North America. The VSI research agenda encompasses the use of verification in all phases of software construction from requirements elicitation to modeling, design, implementation, testing, integration, certification, and evolution. The primary deliverables of the project are a comprehensive theory of software correctness, a coherent suite of high quality verification tools, and a compelling body of experiments validating the theory and the tools. In this talk, we map the key research challenges for the VSI project.