Verified Concurrent Programmes: Laws of Programming with Concurrency

June 13, 2013
Tony Hoare | MSR Cambridge

The talk starts with a summary of the familiar algebraic properties of choice in a program and of both sequential and concurrent composition. These properties validate the proof rules of Hoare logic (augmented by concurrency), as well as the transition rules of a process algebra (augmented by sequential composition). The laws are then proved true of a simple causal model of the behaviour of programs when executed. The model is generic, and can be particularised to different programming languages, and different notions of correctness. This theoretical result gives hope that any Software Engineering tool that is based on the laws can safely interwork with any other such tool.

Speaker Details

Tony Hoare’s computing interests were stimulated by his first (and only) degree in the humanities (1956): he studied Latin and ancient Greek, followed by philosophy, with particular interest in mathematical philosophy and logic. He learnt Russian during National Service in the Royal Navy. He spent a postgraduate year studying statistics at Oxford and another at Moscow State University, where he discovered the sorting algorithm Quicksort. In 1960, he joined the British Computer industry as a programmer, eventually rising to the rank of Chief Engineer.

His Academic career started in 1968 with appointment as professor at the Queen’s University, Belfast. He chose his long-term research area as proof of the correctness of programs. In the thick of the troubles, he built up a strong computing department, and moved in 1978 to do the same at Oxford. Following the example of Theoretical Physics, his interests broadened to the pursuit of Unifying Theories of Programming.

On reaching retiring age, he accepted an offer of employment at Microsoft Research in Cambridge, where he has seen a strong surge of interest in automation of computer proofs of program correctness. He continues to pursue this interest, while exhorting academic researchers in long-term pursuit of even more idealistic scientific goals.