Keynote: Professor Sir Tony Hoare

Abstract

The ideal of verified software has long been the goal of research in Computer Science. This paper argues that the time is ripe to embark on a Grand Challenge project to construct a program verifier, based on a sound and complete theory of programming, and evaluated by experimental application to a representative sample of useful computer software.

Bibliography

Tony Hoare studied Philosophy, Latin, and Greek at Oxford University in the early fifties, Russian during his National Service in the Royal Navy, and the machine translation of languages as a graduate student at Moscow State University (1959). One outcome of the latter work was the discovery of the Quicksort algorithm.

On returning to England in 1960, he worked as a programmer for Elliott Brothers, and led a team in the development of the first commercial compiler for the programming language Algol 60. In 1968, he took up a Chair in Computing Science at the Queen's University, Belfast. There his output included a series of papers on the use of assertions in program proving. In 1977, he moved to Oxford University, where 'provable correctness' was again a focus of his research. Well-known results of this work included the Z specification language, and the CSP concurrent-programming model. Recently, he has been investigating the unification of a diverse range of theories that apply to different programming languages, paradigms, and implementation technologies.

Throughout his academic career, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He has taken a recent interest in legacy systems, where assertions can play an important role in system testing.

In 1999, on reaching retirement age at Oxford, Tony moved back to industry as a Senior Researcher with Microsoft Research in Cambridge, England. In March 2000, he received a knighthood from the Queen for services to Computing Science.