Verified Software Roadmap

托尼·霍尔（Tony Hoare）教授提出，生产经过验证的软件是计算机科学面临的重大挑战。他概述了一个国际研究计划，结合了许多学科，如编程语言的理论和实现、形式化方法、程序分析和自动定理证明。为了探索Hoare的巨大挑战，2005年秋季在瑞士苏黎世举行了为期五天的IFIP工作会议，并召集了工作小组。该合同允许开发一个经过验证的软件路线图，该路线图概述了一个长期的研究计划，旨在实现关键软件组件的大规模自动化验证，以达到极高的保证水平。本报告是这一系列研究社区会议的成果。该路线图调查了验证理论和实践的最新发展，并列举了为了实现健壮和可扩展的验证技术而必须解决的研究挑战列表。这项工作是作为网络和信息技术研究与发展小组委员会下的高信任软件和系统协调小组的一项合作活动提供资金的。

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.