Mini Workshop on Verified Software

可靠软件的构建构成了21世纪最重大的科学和工程挑战之一。托尼·霍尔教授提出，创造程序验证器是计算机科学的一项重大挑战。他概述了一个国际研究计划，该计划结合了许多学科，如编程语言的理论和实现、形式方法、程序分析和自动定理证明。为了迎接Hoares的重大挑战，2005年秋季在瑞士苏黎世举行了为期五天的IFIP工作会议。会议的重点是确定实现一个成功的程序验证器的实际步骤。工作会议上讨论的主题包括程序规范的进步、验证和改进工具和技术、程序分析、工具集成、指标、里程碑和基准套件。在工作会议之后，成立了小组，以制定经过验证的软件领域研究的详细路线图。该奖项由NITRD高度信任软件和系统机构间协调小组支持，使一系列小型研讨会能够加快这些小组在起草全面路线图方面的活动。

The construction of reliable software poses one of the most significant scientific andengineering challenges of the 21st century. Professor Tony Hoare has proposed thecreation of a program verifier as a grand challenge for computer science. He hasoutlined an international program of research combining many disciplines such asthe theory and implementation of programming languages, formal methods, programanalysis, and automated theorem proving. In order to take on Hoares grandchallenge, an IFIP Working Conference was held over five days during Fall 2005in Zurich, Switzerland. The focus of the conference was on identifying practicalsteps toward the realization of a successful program verifier. Topics discussed atthe working conference included advances in program specification, verification andrefinement tools and techniques, program analysis, tool integration, metrics, milestones,and benchmark suites. Following the working conference, panels were formed to draw up a detailed road map for research in the area of verified software.This award, supported by the NITRD High Confidence Software and Systems interagency coordinating group, enables a series of mini-workshops to expedite the activities of these panels in drafting a comprehensive road map.