Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project

摘要

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.