Verified software: Theories, tools, experiments vision of a grand challenge project

Abstract

The ideal of correct software has long been the goal of research in Computer Science. We now have a good theoretical understanding of how to describe what programs do, how they do it, and why they work.This understanding has already been applied to the design, development and manual verification of simple programs of moderate size that are used in critical applications. Automatic verification could greatly extend the benefits of this technology. This paper argues that the time is ripe to embark on an international Grand Challenge project to construct a program verifier that would use logical proof to give an automatic check of the correctness of programs submitted to it.Prototypes for the program verifier will be based on a sound and complete theory of programming; they will be supported by a range of program construction and analysis tools; and the entire toolset will be evaluated and evolve by experimental application to a large and widely representative sample of useful computer programs.The project will provide the scientific basis of a solution for many of the problems of programming error that afflict all builders and users of software today. This paper starts with an optimistic vision of a possible long-term future of reliable programming. It argues that scientific research will play an essential role in reaching these long-term goals. It suggests that their achievement should be accelerated by a major international research initiative, modelled on a Grand Challenge, with specific measurable goals. The suggested measure is one million lines of verified code.By definition, this consists of executable programs, together with their specifications, designs, assertions, etc., and together with a machine-checked proof that the programs are consistent with this documentation. We anticipate that the project would last more than ten years, consume over one thousand person-years of skilled scientific effort, drawn from all over the world.Each country will contribute only a proportion of the effort, but all the benefits will be shared by all. The paper concludes with suggestions for exploratory pilot projects to launch the initiative and with a call to volunteers to take the first steps in the project immediately after this conference.A possible first step will be to revise and improve this paper as a generally agreed report of goals and methods of the scientists who wish to engage in the project. © IFIP International Federation for Information Processing 2008.