This talk by Professor Cliff Jones from Newcastle University traces the important steps in the history of research on reasoning about programs.
The main focus is on sequential imperative programs. Initially, researchers focused on ways of verifying that a program satisfies its specification (or that two programs were equivalent). Over time it became clear that post facto verification is only practical for small programs and attention turned to verification methods which support the development of programs; for larger programs it is necessary to exploit a notation of compositionality. Coping with concurrent algorithms is much more challenging - this and other extensions are considered briefly.
The main thesis of this talk is that the idea of reasoning about programs has been around since they were first written; the search has been to find tractable methods.
About the speaker
Professor Cliff Jones is a Fellow of the Royal Academy of Engineering (FREng), ACM, BCS, and IET and Founding Editor of the Formal Aspects of Computing journal.
Cliff has spent 20 years of his career in industry. Fifteen years in IBM saw among other things the creation with colleagues in Vienna of VDM which is one of the better known "formal methods". He subsequently became a professor at the University of Manchester, worked in industry at Harlequin for a period and is now a Professor of Computing Science at the University of Newcastle upon Tyne. As well as formal methods (especially concurrency) and their support systems, he also has interests in interdisciplinary aspects of computer science and the history of computing.
This event is open to all and starts at 7.30pm.