Abstract

Verified Software: a Grand Challenge for Computing Research.

Software verification has long been a scientific ideal that drives research in Computing Science. Its goal has been the development of a program verifier capable of certifying that a program satisfies desirable properties that have been clearly stated as its specification. There are now several such verifiers available to assist in scientific research.

To develop these systems for general application by software engineers will require intense collaborative research from specialists in many research communities - for example, theorem proving, constraint satisfaction, model checking, programming methodology, formal methods, compiler design, optimisation, program analysis, testing, and human interface design. All the accumulated results of this research will be embodied in a set of scientifically based tools, for use first by experimental scientists, and eventually by professional programmers.

Even more effort will be needed to experiment and demonstrate the prototype tools by application to a corpus of typical programs in use today. This should be drawn from a wide range of current software, of varying sizes and difficulty, and with varying degrees of partial or total specification. I have suggested a goal of a million lines of verified code as an adequate test of the capability of a mature program verifier. I have suggested that a project on this scale should be organised on the same basis as other Grand Challenges in Physics, Astronomy and Genetics. And these suggestions are currently being explored by leading members of the international research community.

Tony Hoare first took up program verification as a goal for academic research at the start of his academic career in 1968. He welcomed the topic as one that was unlikely to find commercial application until after his date of retirement in 1999. He is delighted that some of the basic concepts of verification are now being incorporated into widely used program analysis tools. The ultimate scientific ideal of program verification now seems ripe for a major intiative.

Biography: Sir Charles Antony Richard Hoare (Tony Hoare or C.A.R. Hoare)

Tony Hoare's interest in computing was awakened in the early fifties, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. He was fascinated by the power of mathematical logic as an explanation of the apparent certainty of mathematical truth. During his National Service (1956-1958), he studied Russian in the Royal Navy. Then he took a qualification in statistics (and incidentally) a course in programming given by Leslie Fox). In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.

On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team (including his later wife Jill) in the design and delivery of the first commercial compiler for the programming language Algol 60. He attributes the success of the project to the use of Algol itself as the design language for the compiler, although the implementation used decimal machine code. Promoted to the rank of Chief Engineer, he then led a larger team on a disastrous project to implement an operating system. After managing a recovery from the failure, he moved as Chief Scientist to the computing research division, where he worked on the hardware and software architecture for future machines.

These machines were cancelled when the Company merged with its rivals, and in 1968 Tony took a chance to apply for the Professorship of Computing Science at the Queen's University, Belfast. His research goal was to understand why operating systems were so much more difficult than compilers, and to see if advances in programming theory and languages could help with the problems of concurrency. In spite of civil disturbances, he built up a strong teaching and research department, and published a series of papers on the use of assertions to prove correctness of computer programs. He knew that this was long term research, unlikely to achieve industrial application within the span of his academic career.

In 1977 he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. With the aid of external funding from government initiatives, industrial collaborations, and charitable donations, Oxford now teaches a range of degree courses in Computer Science, including an external Master's degree for software engineers from industry. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model. A recent personal research goal has been the unification of of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies.

Throughout more than thirty years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.

Tony Hoare received the 1980 ACM Turing Award for "his fundamental contributions to the definition and design of programming languages". In 2000 he was knighted for services to education and computer science.