The construction of reliable software poses one of the most significant scientific and engineering challenges of the 21st century. Professor Tony Hoare has proposed the creation of a program verifier 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 take on Hoares grand challenge, an IFIP Working Conference was held over five days during Fall 2005 in Zurich, Switzerland. The focus of the conference was on identifying practical steps toward the realization of a successful program verifier. Topics discussed at the working conference included advances in program specification, verification and refinement 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.
