Professor Tony Hoare has proposed the production of verified software as a grand challenge for computer science. He has outlined an international program of research combining many disciplines such as the theory and implementation of programming languages, formal methods, program analysis, and automated theorem proving. In order to explore Hoare's grand challenge, an IFIP Working Conference was held over five days during Fall 2005 in Zurich, Switzerland, and working panels were convened. This award enables the development of a Verified Software Roadmap, which outlines a long-term program of research aimed at achieving the large-scale automated verification of critical software components to extremely high levels of assurance. This report is the product of this series of research community meetings. The roadmap surveys recent developments in the theory and practice of verification, and enumerates a list of research challenges that must be addressed in order to achieve robust and scalable verification technology. The effort is funded as a cooperative activity under the High Confidence Software and Systems Coordinating Group under the Networking and Information Technology Research and Development (NITRD) Subcommittee.
