The Verified Software Initiative: A Manifesto

A team of researchers from SRI International Computer Science Laboratory has proposed a long-term research program toward the construction of error-free software systems. The research project, called the Verified Software Initiative, will make an effort to a comprehensive theory of programming that covers the features needed to build practical and reliable programs. It will focus on a coherent toolset that automates the theory and scales up to the analysis of industrial-strength software. It will also develop a collection of realistic verified programs that can replace unverified programs in existing service and continue to evolve in a verified state. Verification involves the rigorous demonstration of the correctness of software with respect to a specification of its intended behavior. It can be applied at all phases of the software lifecycle including design to maintenance.