Verified Software Roadmap

点击翻译按钮获取中文摘要

Professor Tony Hoare has proposed the production of verified software as a grandchallenge for computer science. He has outlined an international program of researchcombining many disciplines such as the theory and implementation of programminglanguages, formal methods, program analysis, and automated theorem proving. Inorder to explore Hoare's grand challenge, an IFIP Working Conference was heldover 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.