Hoare, T., Misra, J., Leavens, G. T., & Shankar, N. (2021). The verified software initiative: A manifesto. In Theories of Programming: The Life and Works of Tony Hoare (pp. 81-92).
Introduction
We propose an ambitious and long-term research program toward the construction of error-free software systems. Our manifesto represents a consensus position that has emerged from a series of national and international meetings, workshops, and conferences held from 2004 to 2007. The research project, the Verified Software Initiative, will attempt to construct over the next fifteen years: (1) a comprehensive theory of programming that covers the features needed to build practical and reliable programs, (2) a coherent toolset that automates the theory and scales up to the analysis of industrial strength software, and (3) a collection of realistic verified programs that could replace unverified programs in current service and continue to evolve in a verified state.
This document summarizes the background of the initiative, its scientific goals, and the principles that underlie a worldwide collaboration to achieve them. We include an assessment of its strengths, weaknesses, threats and opportunities. A companion document will summarize a range of work packages, including developments in theory, tools, and experiments.